In: Lectures on Concurrency and Petri Nets: Advances in Petri Nets, pages 467-495. Volume 3098 of Lecture Notes in Computer Science / Jörg Desel, Wolfgang Reisig, Grzegorz Rozenberg (Eds.) --- Springer-Verlag, June 2004.
Abstract: This work considers model construction and validation in controller design. The problem we are interested in is to derive a formal model of a controlled automation system from a semi-formal description of the uncontrolled plant and various requirements concerning the plant and the processes of the controlled system. These requirements are originally formulated on many different abstraction levels, partly employing formal notations, partly using just natural language and partly consisting of mixtures of both. Moreover, they are often incomplete, contain errors, contradict each other and assume some domain knowledge which is typically not explicitly stated. So a crucial part of the model construction process is the formalization of the plant and of the requirements as well as validation of the derived models. We suggest a simulation-based method which employs formal and graphical representations of process models and specifications and which involves an iterative process of formalization and validation of requirements. The approach is based on particular Petri nets, called signal nets, as formal process models and partially ordered runs as their semantics. This contribution also reports on a case study from the automotive industry.