Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

9-2009

Abstract

In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are sound and complete. We enhance our home-grown PAT model checker with the technique and show its usability via the verification of benchmark systems.

Keywords

Model Check, Transition System, Operational Semantic, Label Transition System, Process Construct

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12

First Page

581

Last Page

600

ISBN

9783642103728

Identifier

10.1007/978-3-642-10373-5_30

Publisher

Springer Link

City or Country

Rio de Janeiro, Brazil

Additional URL

https://doi.org/10.1007/978-3-642-10373-5_30

Download

Share

COinS