This contribution defines for the first time “safety automata”, a specification language for safety control functions. This fills an important gap in the method tool box of the automation engineer. The definition has a profound potential to broaden the use of automata and their well-known advantages in industrial applications. The advantages and application of safety automata are explained by example via the function block SF_Equivalent of the PLCopen specification. Stepwise, the authors illustrate the specification of this function block by means of safety automata, the transformation rules to implement the automata in fully functional PLC code, and finally the generation of test cases that allow checking both the automata and the PLC code.

This paper is presenting a tool called SIMOTEST. It allows the user to conduct Model Based Testing of MatLab/Simulink models. In particular it allows automatically running and evaluating test cases which got generated from a test model. Test cases which get run from SIMOTEST can be used for testing hybrid realtime systems i.e. systems which have continuous and discrete inputs/outputs which need to fulfill timing requirements. This is achieved by using the IEEE Standard for Signal and Test Definition (IEEE 1641).

The current practice of component based engineering raises concerns in industry when the specification of proprietary components suffers from inaccuracy and incompleteness. Engineers face difficulties in producing quality systems when they lack knowledge of the interoperability of components. In order to address this issue, we present a novel framework for iterative refinement of specification for component based systems. The novelty is the use of a preliminary behavioral model as a source for triggering refinement iterations. Moreover, it exploits rigorous formal techniques to achieve high-level system validation as an integral part of the refinement procedure. The framework has been evaluated on an automotive system in which the embedded software control units were developed by third-party vendors. The final results produced an improved formal system specification that identified several behaviors that were previously unknown.

Dependability is often a very abstract concept. The reason is that dependability implications shall be very rare and are often not even wanted to happen during testing. In particular for software-intensive systems, it is very hard to find correct causal relationships/minimal cut sets. Modern model-based approaches help here by computing for example minimal cut sets automatically. However, these methods always rely on a correct model of the environment. In addition, the results are often not traceable or understandable for humans. Therefore, we suggest combining model-based analysis for deriving safety properties with virtual realities for ensuring model validity and trace-ability of results.

In manufacturing automation domain safety and availability are the most important factors to ensure productivity. In modern software intensive networked automation systems it became quite hard to ensure which non-functional requirements are related to these factors as well as whether these are satisfied or not. This is due to the prevalence of manual efforts in several analyses phases where complexity of the system often makes it hard to obtain comprehensive overview and thus makes it difficult to ascertain the presence of certain undesired consequences. Since design, development and following verification and validation activities are largely dependent upon the result of the analyses the product is largely affected. To address these problems automated fault tree generation is presented in this paper. It uses distinct modeling artifacts and information to automatically compose formal models of the system. Embedding hardware and network failures it is then ascertained through model checking whether the system satisfies certain safety and availability properties or not. This information is used to compose the fault tree. Proposed approach will improve completeness and correctness in fault trees and will consequently help in improving the quality of the system. Furthermore, it is also shown how the artifacts of this analysis can be used to produce test goals and test cases to validate the software constituents of the system and assure traceability between testing activity and safety requirements.