Modeling and Formal Verification of Production Automation Systems

This paper presents the real-time model checker RAVEN and related theoretical background. RAVEN augments the efficiency of traditional symbolic model checking with possibilities to describe real-time systems. These extensions rely on multi-terminal binary decision diagrams to represent time delays and time intervals. The temporal logic CCTL is used to specify properties with time constraints. Another noteworthy feature of our model checker is its ability to compose a system description out of communicating modules, so called I/O-interval structures. This modular approach to system description alleviates the omnipresent state explosion problem common to all model checking tools. The case study of a holonic1 material transport system demonstrates how such a production automation system can be modeled in our system. We devise a detailed model of all components present in the described system. This model serves as basis for checking real-time properties of the system as well as for computi...

• Type: Conference
• Year: 2004
• Where: DFG
• Authors: Jürgen Ruf, Roland J. Weiss, Thomas Kropf, Wolfgang Rosenstiel
• Keywords: DFG 2004, Model, Model Checker, Model Checking, Operating System