IIIT Hyderabad Publications |
|||||||||
|
Modular safety verication and liveness testing of real-time industrial manufacturing systems using interval assumptionsAuthors: Santosh Arvind Adimoolam,Venkatesh Choppella, PVR Murthy Date: 2014-05-01 Report no: IIIT/TR/2014/22 AbstractExtant approaches of assume-guarantee style modular model-checking of real-time models specify assumptions as timed or hybrid automata. In this paper, we instead identify interval assumptions, which are a subset of Timed Computational Tree Logic and can succinctly specify the requirements about the environment of the components of a real-time industrial manufacturing system. For industrial manufactur- ing systems, we find that timed automata based specification of assumptions would form clumzier representations, compared to interval assumptions which are a neater in their representation. Also, interval assumptions can be discharged easily by model-checking and model-checking has efficient tool support. But timed-automata assumptions are discharged by simulation-checking, which does not have efficient tool support. We introduce continuous pure signal input output automata (CPSIOA) for modeling the components of an industrial manufacturing system, so that interval assumptions can express the assumptions about the environment of the CPSIOA models. Then using a tableau CPSIOA construction encoding an interval assumption, we can verify safety guarantees and test progress dependent liveness guarantees under the interval assumption via model-checking. The applicability of our approach is corroborated by implementing on the Turntable and Production Cell that are standard small scale examples of industrial manufacturing systems. Full report: pdf Centre for Software Engineering Research Lab |
||||||||
Copyright © 2009 - IIIT Hyderabad. All Rights Reserved. |