Skip to Main content Skip to Navigation
Conference papers

A Formal Approach for the Development of Automated Systems

Abstract : This paper deals with the use of two verification approaches : theorem proving and model checking. We 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, we propose to apply the language TLA+ to verify liveness properties on a software behavior. We extend first of all the expressivity of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we give transformation rules from a temporal B model into a TLA+ module. We present in particular, our prototype system called B2TLA+, that we have developed to support this transformation. Finally, we verify these properties thanks to the TLC model checker.
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/inria-00158908
Contributor : Olfa Mosbahi <>
Submitted on : Monday, July 2, 2007 - 12:22:46 AM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
Long-term archiving on: : Monday, September 24, 2012 - 10:47:01 AM

File

paper_382.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00158908, version 1

Collections

Citation

Olfa Mosbahi, Leila Jemni, Jacques Jaray. A Formal Approach for the Development of Automated Systems. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, INSTICC - Institute for Systems and Technologies of Information, Control and Communication, Jul 2007, Barcelone, Spain. pp.304-310. ⟨inria-00158908⟩

Share

Metrics

Record views

407

Files downloads

349