LAUSR

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.