Requirements for a Temporal B Assigning Temporal Meaning to Abstract Machines … and to Abstract Systems

摘要

Abstract Machines Notation (AMN) is the notation of the B method for specifying systems and it is supported by tools providing editing, navigating, animating and proving facilities. AMN permits us to state invariance properties, based on safety conditions, but there are applications, such as telecom services or distributed systems, where fairness and eventuality properties must also be considered. We define a way to extend the B method expressivity by defining a semantics over traces, in the same spirit as the temporal logic of actions does and we provide a semantical framework for defining a extended B method that can exploit the B environments facilities. We analyse requirements for developing effective temporal facilities extending the scope of B and we found our experiment on case studies related to telecommunications services, which provide a framework for getting requirements on the expressivity of the description language for service properties.