Formal Methods for Verifications of Reactive Systems

View Sample PDF

Author(s): Olfa Mosbahi (Nancy University, France & Martin Luther University, Germany)and Mohamed Khalgui (Martin Luther University, Germany)
Copyright: 2011
Pages: 40
Source title: Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility
Source Author(s)/Editor(s): Mohamed Khalgui (Xidian University, China)and Hans-Michael Hanisch (Martin Luther University, Germany)
DOI: 10.4018/978-1-60960-086-0.ch014

Keywords: Computer Science & IT / Information Science Reference / Systems & Software Design / Systems and Software Engineering

Purchase

View Formal Methods for Verifications of Reactive Systems on the publisher's website for pricing and purchasing information.

Abstract

This chapter deals with the use of two verification approaches: theorem proving and model checking. The authors focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA+ by using its model checker TLC. By considering the limitation of the Event-B method to invariance properties, the authors propose to apply the language TLA+ to verify liveness properties on a software behavior. The authors extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, they give transformation rules from a temporal B model into a TLA+ module. The authors present in particular, their prototype system called B2TLA+, that they have developed to support this transformation; then they can verify these properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, they propose the use of the predicate diagrams. The authors illustrate their approach on a case study of a parcel sorting system.

The IRMA Community

Research IRM

Formal Methods for Verifications of Reactive Systems

Purchase

Abstract

Related Content

IRMA Sponsors