AbstractIn this paper we address the problem of scheduling and synthesizing distributed control programs for a batch production plant. We use a timed automata model of the batch plant and the verification tool UPPAAL to solve the scheduling problem.
In modeling the plant, we aim at a level of abstraction which is sufficiently accurate in order that synthesis of control programs from generated timed traces is possible. Consequently, the models quickly become too detailed and complicated for immediate automatic synthesis. In fact, only models of plants producing two batches can be analyzed directly! To overcome this problem, we present a general method allowing the user to guide the model-checker according to heuristically chosen strategies. The guidance is specified by augmenting the model with additional guidance variables and by decorating transitions with extra guards on these. Applying this method have made synthesis of control programs feasible for a plant producing as many as 60 batches.
The synthesized control programs have been executed in a physical plant. Besides proving useful in validating the plant model and in finding some modeling errors, we view this final step as the ultimate litmus test of our methodology's ability to generate executable (and executing) code from basic plant models.
Categories and Subject Descriptors: D.1.2 [Programming Techniques]: Automatic Programming; D.2.2 [Software Engineering]: Tools and Techniques; D.2.4 [Software Engineering]: Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; I.6.4 [Simulation and Modeling]: Model Validation and Analysis; J.6 [Computer-Aided Engineering]
Additional Key Words and Phrases: real-time verification, guided model-checking, scheduling, program synthesis, distributed systems
Selected references
- Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 25 April 1994. Fundamental Study.