Safe operation sequences: a generation approach based on iterative refinements and abstractions of timed automata. Issue 1 (July 2017)

• Record Type: Journal Article
• Authors: Cochard, Thomas; Gouyon, David; Pétin, Jean-François
• Is Part Of: IFAC-PapersOnLine. Volume 50:Issue 1(2017)
• Page Start: 6952
• Page End: 6957
• Publication Date: 2017-07
• Subjects: Action sequences generation -- Iterative refinement -- Reachability analysis -- Model checking -- Timed automata; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2017.08.1335
• Languages: English
• ISSNs: 2405-8963

Abstract

Abstract: Operation procedure engineering for complex and critical systems aims to provide action sequences satisfying safety requirements specifications. If automatic generation of procedure seems to be interesting for this purpose, the limit of the use of formal generation approaches is classically the combinatorial explosion induced by the size and the number of required models. This article addresses this issue by proposing an iterative approach for the generation of safe operation sequences, using timed automata, and based on reachability analysis. The originality of this approach is to combine a bottom-up framework to build progressively system models by abstraction, and a top-down iterative action sequence generation.