@InProceedings{GKN02_ag,
AUTHOR = {Giese, Holger and Kardos, Martin and Nickel, Ulrich A.},
TITLE = {{Integrating Verification in a Design Process for Distributed Production Control Systems}},
YEAR = {2002},
MONTH = {April},
BOOKTITLE = {Proc. of Second International Workshop on Integration of Specification Techniques for Applications in Engineering (INT2002), Grenoble, France},
PDF = {INT02.pdf},
ABSTRACT = {The specification of software for distributed production control systems is an error prone task. The ISILEIT project aims at the development of a seamless methodology for integrated design, analysis and validation of distributed production control systems. Ensuring the correctness of the design at the earliest stage possible is a major challenge in any software development process. Formal verification is very appealing in this context in addition to simulation and testing, since it implies an exhaustive exploration of all possible behaviours of a system model. This paper presents a proposal of how to use Abstract State Machines to build a series of formal semantics of our specification language, which comprises a subset of SDL and UML. We will further explain, how the use of Abstract State Machines permits model checking at different levels of abstraction, which therefore can be better integrated into the overall design process of distributed production control systems.}
}