@inproceedings{8168b1826edc402593c2b40aa75482c2,
title = "A Model for Industrial Real-Time Systems",
abstract = "Introducing automated formal methods for large industrial real-time systems is an important research challenge. We propose timed process automata (TPA) for modeling and analysis of time-critical systems which can be open, hierarchical, and dynamic. The model offers two essential features for large industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) an automated state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating control processes which can activate other processes. We show how to automatically establish safety and reachability properties of TPA by reduction to solving timed games. To mitigate the state-space explosion problem, an automated state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed.",
keywords = "Automated formal methods, Timed process automata, State-space reduction, Compositional modeling, Timed games, Automated formal methods, Timed process automata, State-space reduction, Compositional modeling, Timed games",
author = "{Bin Waez}, {Md Tawhid} and Andrzej Wasowski and Juergen Dingel and Karen Rudie",
year = "2015",
doi = "10.1007/978-3-662-46081-8_9",
language = "English",
isbn = "978-3-662-46080-1",
volume = "8931",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "153--171",
editor = "Deepak D'Souza and Akash Lal and {Guldstrand Larsen}, Kim",
booktitle = "Verification, Model Checking, and Abstract Interpretation",
address = "Germany",
}