Article ID Journal Published Year Pages File Type
551856 Information and Software Technology 2011 20 Pages PDF
Abstract

ContextThis paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA+ to verify liveness properties on Event-B models.ObjectiveThis paper deals with the use of two verification approaches: theorem proving and model-checking, in the construction and verification of safe reactive systems. The theorem prover concerned is part of the Click_n_Prove tool associated to the Event-B method and the model checker is TLC for TLA+ models.MethodTo verify liveness properties on Event-B systems, we 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, we propose semantics of the extension over traces, in the same spirit as TLA+ does. Third, we give verification rules in the axiomatic way of the Event-B method. Finally, 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; then we can verify liveness properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams and its associated tool DIXIT. As the B refinement preserves invariance properties through refinement steps, we propose some rules to get the preservation of liveness properties by the B refinement.ResultsThe proposed approach is applied for the development of some reactive systems examples and our prototype system B2TLA+ is successfully used to transform a temporal B model into a TLA+ module.ConclusionThe paper successfully defines an approach for the specification and verification of safety and liveness properties for the development of reactive systems using the Event-B method, the language TLA+ and the predicate diagrams with their associated tools. The approach is illustrated on a case study of a parcel sorting system.

Related Topics
Physical Sciences and Engineering Computer Science Human-Computer Interaction
Authors
, , ,