An overview of the SystemB collaborative project

Much research work has been done on linking UML and formal methods but few have focused on using formal methods to check the integrity of UML models so that the models can be verified. A current collaborative project between the University of Surrey and AWE plc is investigating the underpinning of xUML platform independent models with CSP װ B specifications. Our position paper presents an overview of the project and demonstrates an opportunity for applying formal methods in industry. One of the project’s aims is to support reasoning about concurrent xUML state machines. xUML is a subset of UML which provides support for code generation. AWE has already developed mappings between xUML and SPARK Ada and our current work will provide further techniques in order to ensure the safety of their software systems. UML has become the language of choice for systems engineers at AWE and support for formal techniques is necessary.