Reducing Time to Market through Formal Methods
Model Based Software Engineering (MBSE) integrates simulation, automation, and traceability into the development process. By using tools like Simulink and Stateflow developers can simulate system behaviour, automate code generation and maintain traceability from requirements to implementation. The major drawback with MBSE is showing not only that it does what is required, but much more importantly from a certification perspective, that it does not have unwanted functionality, including showing what happens when, not ‘if’ things go wrong. This challenge is caused by the semantics of the models being unclear, the link between the model and the requirements often being obscure and being able to show that code generated correctly implements the requirements for the model in an efficient and effective manner. The key is to leverage MBSE through evaluating verification artefacts generated by MBSE using Automated Reasoning. A key application of this approach to Robotic and Autonomous Systems is discussed in terms of commercial impact.