The IRMA Community
Newsletters
Research IRM
Click a keyword to search titles using our InfoSci-OnDemand powered search:
|
Formal Methods for Verifications of Reactive Systems
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.
Related Content
Babita Srivastava.
© 2024.
21 pages.
|
Sakuntala Rao, Shalini Chandra, Dhrupad Mathur.
© 2024.
27 pages.
|
Satya Sekhar Venkata Gudimetla, Naveen Tirumalaraju.
© 2024.
24 pages.
|
Neeta Baporikar.
© 2024.
23 pages.
|
Shankar Subramanian Subramanian, Amritha Subhayan Krishnan, Arumugam Seetharaman.
© 2024.
35 pages.
|
Charu Banga, Farhan Ujager.
© 2024.
24 pages.
|
Munir Ahmad.
© 2024.
27 pages.
|
|
|