Wyniki wyszukiwania - BazTech

1

SyLVaaS : System Level Formal Verification as a Service

Mancini T., Mari F., Massini A., Melatti I., Tronci E.

Fundamenta Informaticae

|

2016

|

Vol. 149, nr 1/2

101--132

EN

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variations in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to (Hardware In the Loop Simulation based) System Level Formal Verification. SyLVaaS takes as input a finite state automaton defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion (i.e., with no communication among the parallel processes) on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).

2

Flexible Plan Verification: Feasibility Results

Cesta A., Fratini S., Orlandini A., Finzi A., Tronci E.

Fundamenta Informaticae

|

2011

|

Vol. 107, nr 2/3

111-137

EN

Timeline-based planning techniques have demonstrated wide application possibilities in heterogeneous real world domains. For a wider diffusion of this technology, a more thorough investigation of the connections with formal methods is needed. This paper is part of a research program aimed at studying the interconnections between timeline-based planning and standard techniques for formal validation and verification (V&V). In this line, an open issue consists of studying the link between plan generation and plan execution from the particular perspective of verifying temporal plans before their actual execution. The present work addresses the problem of verifying flexible temporal plans, i.e., those plans usually produced by least-commitment temporal planners. Such plans only impose minimal temporal constraints among the planned activities, hence are able to adapt to on-line environmental changes by trading some of the retained flexibility. This work shows how a model-checking verification tool based on Timed Game Automata (TGA) can be used to verify such plans. In particular, flexible plan verification is cast as a model-checking problem on those automata. The effectiveness of the proposed approach is shown by presenting a detailed experimental analysis with a real world domain which is used as a flexible benchmark

3

Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections

Bobbio A., Ciancamerla E., Minichino M., Tronci E.

Archives of Transport

|

2005

|

Vol. 17, iss.3-4

39-55

EN

Communication networks, usually born for not critical aims, are more and more used in domains which are critical for safety, availability, timeliness and quality of service. In automotive domain, Tele Control Systems (TCS), based on communication networks, are proposed in prototypal fashion, for vehicle controI inside safety critical transport infrastructures, such as long bridges and tunnels. Such systems, typically, consist of one or more Infrastucture Control Centres (ICC), aIlocated nearby the infrastructure, interconnected to the vehicles to be controlled (the mobile nodes), by a Mobile Network, even Public (PMN). In such a case, PMN is the heart of the system, makes the system more vulnerable because of many factors (complexity, mobility of nodes, response time, and public access to the network), and then requires to be highly performable and dependable. The paper discusses performability and safety measures of a PMN, computed by stochastic and functional analysis. PMN implements GSM and GPRS connections and represents the most innovative and challenging aspects of a Tele ControI System, inside a safety critical transport infrastructure.

PL

Autorzy rozpatrują miary sprawności działania i bezpieczeństwa publicznej sieci komórkowej za pomocą analizy stochastycznej i funkcjonalnej. Prezentowana publiczna sieć komórkowa implementuje połączenia sieci GSM i GPRS oraz reprezentuje najbardziej innowacyjne i konkurencyjne elementy telekomunikacyjnego systemu sterowania wewnątrz infrastruktury transportowej w aspekcie jej bezpieczeństwa.