Despite the large amount of models for different aspects of factory automation systems, many of these models target at individual and in most cases static aspects of the system, such as the geometry or its electric parts. There is a lack of suitable description methods, which integrate these individual models to a behavior model including spatial aspects and the handling of material. Furthermore, it is important that this model keeps the link to the more detailed individual models and is sufficiently formal in order to allow an automated analysis. This paper provides a solution to this problem by introducing a model which addresses both spatial structure and behavior and is based on a thorough mathematical theory. Complementary, we report on a tool realization of the modelling theory and explain how the model supports the development of mechatronic systems.

During testing, the execution of valid cases is only one part of the task. Checking the behavior in boundary situations and in the presence of errors is an equally important subject. This is especially true in embedded systems where parts of a system's function are realized by sensors and actuators, which are subject to wear and defects. As testing with the real hardware is costly and hardware defects are hard to stimulate, such tests are often performed using behavior models of the system which allow to execute the controller software against simulated hardware and environment. However, these models seldom contain possible hardware errors, as this makes the models more complex and, thus, harder to create and maintain. This paper presents a modeling technique for the description of system errors without modifying the original model. Error specifications for individual system components are modeled separately and can be used to augment the system model.

Scenario-based specifications have gained wide acceptance in requirements engineering. However, scenarios are not appropriate to describe global, system-wide invariants. Thus, a specification often consists of scenarios and universal properties. In order to obtain a consistent specification, the scenarios must be integrated in a way which does not violate the properties. However, manual integration of scenarios is an error-prone and laborious process. In the presented paper we suggest a synthesis algorithm for automatic integration of system scenarios to an overall specification with guaranteed satisfaction of system-wide safety properties. The main idea is to compute inter-scenario priorities, which disable certain scenarios if they violate a property.

Abstract Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.