This Field Report summarizes the current situation of the industrial usage of Formal Methods and Automatic Test and Validation Software Tools (Analysis Tools) in the Embedded Market. In most cases the usage of Formal Method and ATG Tools is related to a Model Based Development Process and related to Front-end Modeling Tools.
This report gives an overview of the current technological and methodological practice of these analysis tools and techniques in the Embedded Systems domain. The presented methods and results have been observed and collected over more than 10 years project experiences in different industrial domains.
The Model-based software development process for embedded systems is a strong growing approach and soon, it will be state-of-the-art that model-based development processes are established and exercised. If we also consider that the current strong trend to automation of safety-critical functions requires stringent application of safety standards then it will become common practice for embedded software engineers and test engineers to develop and verify their software using new testing technologies like formal verification and automatic test generation.
Benefits of these technologies are obvious: design flaws are detected early in the overall process. The quality of models and software – either generated automatically or developed manually – increases drastically. More and more Safety Critical Applications which are taken place e.g. in the automotive industry force the OEM’S to introduce state of the art technology regarding safety, so automatic validation technologies like model checking and automatic safety analysis will become a standard technology to ensure safety on the modeling level within an established model based development process.
It has been figured out in this field report that Automatic Model Validation based upon formal methods is the key to develop Reference Models for later design phases. These Reference Models are the input for a black-box automatic test generation approach since these models are fulfilling their functional requirements. The generated input and expected output test case can be applied on any implementation of the models behavior for validating that the software behaves correct. The overall outcome of the usage of Formal Methods and Automatic Test Case Generation techniques and technologies is a significant cost reduction in the development process of Embedded
Systems.