Model-based system analysis using Chi and Uppaal: An industrial case study

New methods and techniques are needed to reduce the integration and test effort (lead time, costs, resources) in the development of high-tech multi-disciplinary systems. To facilitate this effort reduction, a method called model-based integration and testing is being developed. The method allows to integrate formal and executable models of system components that are not yet physically realized with available realizations of other components. The combination of models and realizations is then used for early analysis of the integrated system by means of validation, verification, and testing. The analysis enables early detection and prevention of problems that would otherwise occur during real integration, resulting in a significant reduction of effort invested in the real integration and testing phases. This paper illustrates the application of the method to a realistic industrial case study, focusing on verification of the models obtained. We show how a system model has been developed for model-based integration and testing in the timed process algebra χχ (Chi), and how certain behavioral properties of this model have been verified by the Uppaal model checker.