Showing 1–2 of 2 results for author: Rayana, S B
-
Compositional Verification for Timed Systems Based on Automatic Invariant Generation
Authors:
Lacramioara Astefanoaei,
Souha Ben Rayana,
Saddek Bensalem,
Marius Bozga,
Jacques Combaz
Abstract:
We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints i…
▽ More
We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented in the RTD-Finder tool and successfully experimented on several benchmarks.
△ Less
Submitted 16 September, 2015; v1 submitted 16 June, 2015;
originally announced June 2015.
-
Timed Orchestration for Component-based Systems
Authors:
Chih-Hong Cheng,
Lacramioara Astefanoaei,
Harald Ruess,
Souha Ben Rayana,
Saddek Bensalem
Abstract:
Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We forma…
▽ More
Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Parameter synthesis problems for interaction-level LTL properties are translated to parameter synthesis problems for state-based safety properties. For safety properties, synthesis problems are solved by checking satisfiability of $\exists\forall$SMT constraints. For constraint generation, we provide a set of computationally cheap over-approximations of the set of reachable states, together with fence constructions as sufficient conditions for safety formulas. We demonstrate the feasibility of our approach by solving typical machine configuration problems as encountered in industrial automation.
△ Less
Submitted 20 May, 2016; v1 submitted 21 April, 2015;
originally announced April 2015.
