Object Modelling in the SystemB Industrial Project

Abstract

The SystemB project is a two year project at the University of Surrey, funded by AWE plc, and is concerned with bridging the areas of formal methods and object modelling. The project is focused on the CSP ∥ B integrated formal method and increasing its level of tool support so that CSP ∥ B models of Executable UML (xUML) systems can be constructed automatically. The CSP ∥ B models will subject the xUML model to formal analysis prior to generating executable code. We are currently developing a CSP ∥ B model generator within the xUML toolsuite provided by Kennedy Carter Ltd. xUML is used within AWE and we will initially focus on reasoning about xUML state machines. Actions within xUML state machines are defined using the Action Specification Language (ASL). ASL is more low level than the Object Constraint Language; they can execute concurrently, and can also be used in operation definitions. Hence it is a challenge to model formally. In the extended abstract we provide an overview of one ASL to AMN translation pattern being developed and highlight the role of B in the project.