Model Checking UML Designs
Real-time embedded systems are increasingly prevalent in military and civilian applications. They are often both complex and safety critical in both military applications (missile guidance systems, weapon control systems, etc.) and civilian applications (flight control systems, automotive braking systems, etc). To deal with their inherent complexity and safety requirements, these applications require an advanced design process and sophisticated software-engineering tools to support the process. Such a process would be characterized by rigorous and complete specification capabilities, robust automated translation from design to implementation, support for debugging of the designs at the semantic level of the design specification language, and sophisticated verification and analysis of design models.
In the domain of embedded-systems design, the Unified Modeling Language (UML) is a first step towards these goals; however it does not adequately support the specification requirements of complex embedded systems. Rational Software has attempted to address this by embedding the ROOM methodology for concurrent embedded systems in its UML-RealTime extension to UML and Rose RealTime UML tool. Rose RT is a best of breed COTS tool that builds upon UML-RealTime by adding robust automated code generation and support for simulation and debugging at the UML semantic level.
Current best practices and tools are inadequate for complex mission critical embedded applications because they do not provide adequate verification and analysis of the design models. This lack of support for automated verification and analysis undermines the specification capabilities of current COTS tools. Rational Rose for RealTime allows users to specify the language (in state machine form) of the communication protocol with which components (referred to as capsules in Rose for Realtime) interact. Despite being a powerful design specification capability, this is rarely used in practice because there is no way of ensuring that the components' behaviors will actually obey this protocol. The lack of formal verification capabilities has reduced a powerful design specification technique to mere documentation. This reduced level of specification and complete lack of verification capabilities undermines the safety critical requirements of today's compex embedded systems.
Under a NAVSEA SBIR Phase I contract, GrammaTech is integrating model checking Rational Rose for RealTime Our vision is to have model-checking technology tightly integrated with cutting edge design environments that support automatic code generation. The goal is to decrease the error rate in software designs, and then to use automatic code generation to ensure design-to- implementation consistency. We believe this will have a significant impact on both software engineer productivity and overall software quality.