Formal Specification. The purpose of the formal specification phase is to model the cruise control system in Event-B [Abr09b]. Our input for a formal specification of the cruise control system in Event-B is the semi-formal specification which has been de- rived from the informal specification by the process described in Section 4.3. During pilot deployment we developed several guidelines for constructing for- mal specifications in Event-B from semi-formal specifications in our extended Problem Frames approach which will be described in the following. The first step in constructing a formal specification of a control system in Event-B is to think of the refinement strategy, i.e., a strategy about structur- ing the refinement levels of a formal specification in Event-B. Since Event-B supports so called contexts which describe the static aspects of the system to be modelled and so called machines which describe the dynamic aspects of the system to be modelled one has to think about a refinement strategy for contexts as well as one for machines. During our first experiments of formally modelling the cruise control system in Event-B we found out that our semi-formal requirements specification with different abstraction levels can be mapped to a formal specification in Event-B in the following way: • Each problem diagram is modelled as a separate machine with its as- sociated context. • Elaborations of an abstract diagram into a more concrete one are real- ized in Event-B by refinement of the machine and its associated con- text. • Projections of a problem diagram into two or more subproblems are re- alized in Event-B by shared-variable decomposition [Abr09a] with some changes. • Each phenomenon defined in a problem diagram is modelled either as a constant or a variable in Event-B. • Abstract phenomena which will be elaborated later are realized in Event-B using records. • Elaborations of phenomena in problem diagrams are realized in Event- B using data refinement. • Requirements stated in problem diagrams are realized in Event-B by events and/or invariants. Table 4.2 shows this mapping of Problem Frame elements to Event-B elements in a compact form. We applied this refinement strategy on the cruise control system. Figure
Formal Specification. Modelling in Event-B typically stars from an initially very abstract representation and is conducted in a series of refinement steps, each adding more detail to the model, until the final model is reached containing all details required for coding or, ideally, automatic code generation. In contrast to this “top-down” modelling methodology, which results in a hierarchy of increasingly more complex models, the XCore ISA is “flat”, i.e. the complete specification is presented at the full level of detail. This left the challenge of developing a meaningful method of decompo- sition and abstraction, so that “top down” stepwise refinement could be applied to
