Loading...
Please wait, while we are loading the content...
Similar Documents
Forward and Time-Jumping Symbolic Model Checking for Real Time Systems
| Content Provider | CiteSeerX |
|---|---|
| Author | Logothetis, Georgios |
| Abstract | Abstract. Synchronous languages are widely used in industrial applications for the design and implementation of real-time embedded and reactive systems and are also well-suited for real-time verification purposes, since they have clean formal semantics. In this paper we focuse on the real-time temporal logic JCTL, which can directly support the real-time formal verification of synchronous programs for the design of systems in earlier (high-level) as well as in later (lowlevel) design stages, creating a bridging between industrial real-time descriptions and formal real-time verification. We extend the model-checking capabilities of JCTL, by introducing new forward symbolic model-checking techniques, allowing JCTL to benefit from both, forward–, as well as traditional backward state traversal methods and of course, their combination. In addition to this, we also introduce special methods that allow the algorithms for model-checking JCTL formulae to perform time-jumps during the state space traversal. In other words, the algorithms are able to perform less iterations than the length of the traversed paths (measured in time units). 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Symbolic Model-checking Technique Traversed Path Synchronous Program Real-time Verification Purpose Real-time Temporal Logic Jctl Formal Real-time Verification Time-jumping Symbolic Model Checking Special Method Real-time Formal Verification Time Unit Clean Formal Semantics State Space Traversal Model-checking Jctl Formula Industrial Application Model-checking Capability Reactive System Real Time System Synchronous Language Traditional Backward State Traversal Method Industrial Real-time Description Design Stage |
| Content Type | Text |
| Resource Type | Article |
