How scheduling theory, scenarios, model checking and slicing can help in the verification of RTS

Опубликовано 7 сентября 2016, 16:42

Critical systems are present in an increasing variety of application domains like electronics, control, avionics, health equipment, etc. They are mostly embedded systems, controlling devices that may risk lives or damage assets, hence termed safety-critical systems. These applications generally involve concurrency aspects, as well as complex real-time requirements that challenge the development process. Traditional analytical tools (e.g., Rate Monotoinic Analysis) are not well-suited when trying to verify complex end-to-end requirements involving several interconnected execution-time entities. On the other hand, more sophisticated analysis based on model checking usually consumes prohibitive computational resources when applied to large systems. Moreover, unambiguous description of promised or expected QoS properties -beyond single task deadline satisfaction- requires advanced modeling and mathematical skills. In this talk, I will present key ideas underlying the tool suite VinTime {dependex.dc.uba.ar/vintime/} that attacks the usability and scalability problems from multiple angles, simplifying the definition and verification of real-time systems' designs and properties. VinTime is the result of the integration of loosely coupled tools that share Timed Automata (TAs) as the modelcheckable kernel formalism. Lapsus is a sort of compiler that generates conservative TA models from software architecture views of RT-systems using the underlying scheduling theory for fixed priority application models. In the resulting models, neither the scheduler nor the priorities of tasks are explicitly represented. However, their influence on task response-times is conveyed the timed automata  in the form of time restrictions and invariants. Indeed, following a separation of concerns criterion, we regard the scheduler and the priority assignment mainly as a way to achieve fair computation with predictive response times.  I will explain how generated models can be efficiently checked against complex event-based requirements using model checkers such as Kronos, UPPAAL or Zeus (a distributed timed model checker developed by our research group), after being preprocessed by our property-preserving model-reduction tool, ObsSlice. VTS is a visual language to define complex event-based requirements for RT-systems (e.g., freshness, bounded response, correlation, etc.).  The formalism is based on partial orders and supports real time constraints. Users either describe generic negative scenarios standing for QoS  violations, or conditional scenarios to predicate that one of the situations in a  set is expected to ocurr whenever the antecedent (trigger)  scenario is matched. The associated tool translates conditional VTS specifications into a set of negative scenarios, which are in turn translated into observer TAs.  Thus, the resulting TAs can be composed with the model under analysis (in this toolset, generated by Lapsus) in order to check the satisfaction of the requirements originally stated in VTS. ObsSlice optimizes formal models (in this toolset, networks of TAs generated by Lapsus) with respect to a property to check (in this toolset, generated by VTS)  using an exact abstraction procedure. Thus, TA models are reduced and the verification phase is sped up without compromising the soundness of results.The fact that Lapsus behavioural models are rather loosely coupled (the scheduler is not explicit) makes them particularly well suited to be treated by ObsSlice -or, in general, by any cone-of-influence technique. That is, one of the most appealing aspect of the VinTime approach is that usually only a small subset of components is really needed to perform the model checking, which dramatically reduces the cost of that step. Hence, the complexity of our approach mainly depends on the number of components involved in the requirement instead of the size of the complete model, making it more scalable.