Computer-Aided Analysis and Validation of Heterogeneous System Specifications.

In applications of formal methods, the problem of how to establish the correctness of the initial formalization step is an often underestimated aspect of the system design process. We propose a methodology based on the construction of a mathematical model which reflects the given system so closely that the correctness can be established by observation and experimentation (ground model). Complex technical systems are often heterogeneous, so that different system aspects are best modelled by means of different techniques. This leads to heterogeneous ground models. To achieve a consistent and coherent view of heterogeneous behavioural models, which is a prerequisite for any systematic analysis and validation, we introduce a common semantic framework (meta-model) based on the notion of Abstract State Machines. We exemplify our methodology by an industrial case study from automated manufacturing, the distributed control for a material flow system (MFS). [ABSTRACT FROM AUTHOR]