Experiences in integrating auto-translated state-chart designs for model checking
Paula J. Pingree, Edward G. Benowitz · 2003
Abszruct- In the complex environment of JPL’s flight missions with increasing dependency on advanced software designs, traditional software validation methods of simulation and testing are being stretched to adequately cover the needs of software development. Our aim is to apply formal method techniques and tools to validate mission-specific components of flight software that are specified using finite state machine representation. We have established an automatic translation toolset called Hi Vy that translates Stateflow@ state-charts to Promela, the input language of the Spin model-checker, for the validation of mission-specific components. An interesting challenge in our method is to achieve the closed-loop system model required for Spin. We provide methods to integrate auto-translated Stateflow model specifications with C-code called by the state-charts, and the rest of the model environment which may be auto-translated or included directly in Promela. Index Terms-model checking, statecharts, translation, verification