A Uniform Approach for Specification and Design of Interactive Systems: the B Method

: We have experienced the B Method on a case study which was defined by the French working group on formalisms for interactive systems, i.e. a Post-It® Notes like collaborative application. This experience showed that the B approach allows to cover the description, the formal specification, and the design of each component of basic architecture models, i.e., the five components of the Arch model. Moreover, it has shown that the proposed approach is capable to formally handle large case studies and generate proof obligations which, when proved --automatically-- allows to assert the correctness of the development, and the checking of several user requirements. Keywords : B method, specification refinement, software architecture, interaction properties verification, case study, specification of interactive system. 1 . Introduction The past four editions of DSV-IS Workshops have largely focused on formal specification for Interactive Systems. The first approaches attempted to define new ..