Welcome to the InfoSci Platform
Formal Methods for Verifications of Reactive Systems

Formal Methods for Verifications of Reactive Systems

Olfa Mosbahi, Mohamed Khalgui
Copyright: © 2011 |Pages: 40
ISBN13: 9781609600860|ISBN10: 160960086X|EISBN13: 9781609600884
DOI: 10.4018/978-1-60960-086-0.ch014
Cite Chapter Cite Chapter

MLA

Mosbahi, Olfa, and Mohamed Khalgui. "Formal Methods for Verifications of Reactive Systems." Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility, edited by Mohamed Khalgui and Hans-Michael Hanisch, IGI Global, 2011, pp. 376-415. https://doi.org/10.4018/978-1-60960-086-0.ch014

APA

Mosbahi, O. & Khalgui, M. (2011). Formal Methods for Verifications of Reactive Systems. In M. Khalgui & H. Hanisch (Eds.), Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility (pp. 376-415). IGI Global. https://doi.org/10.4018/978-1-60960-086-0.ch014

Chicago

Mosbahi, Olfa, and Mohamed Khalgui. "Formal Methods for Verifications of Reactive Systems." In Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility, edited by Mohamed Khalgui and Hans-Michael Hanisch, 376-415. Hershey, PA: IGI Global, 2011. https://doi.org/10.4018/978-1-60960-086-0.ch014

Export Reference

Mendeley
Favorite

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.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.