Formal Specification and Verification Method for Hard Real-time Systems

摘要

Hard real-time systems have ongoing interactions with external environments, and consist of concurrent processes. It is important to verify whether hard real-time systems satisfy safety and liveness properties or not. In this paper, we integrally specify concurrency, timing constraints, functions by generalizing our timed statechart. Moreover, we represent opera- tional semantics of timed statechart using Pnueli's clocked transition systems.