|
Records |
Links |
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
|
|
Title |
On Checking Equivalence of Simulation Scripts |
Type |
Journal Article |
|
Year |
2021 |
Publication |
Journal of Logical and Algebraic Methods in Programming |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
100640 |
|
|
Keywords |
Formal verification, Simulation based formal verification, Formal Verification of cyber-physical systems, System-level formal verification |
|
|
Abstract |
To support Model Based Design of Cyber-Physical Systems (CPSs) many simulation based approaches to System Level Formal Verification (SLFV) have been devised. Basically, these are Bounded Model Checking approaches (since simulation horizon is of course bounded) relying on simulators to compute the system dynamics and thereby verify the given system properties. The main obstacle to simulation based SLFV is the large number of simulation scenarios to be considered and thus the huge amount of simulation time needed to complete the verification task. To save on computation time, simulation based SLFV approaches exploit the capability of simulators to save and restore simulation states. Essentially, such a time saving is obtained by optimising the simulation script defining the simulation activity needed to carry out the verification task. Although such approaches aim to (bounded) formal verification, as a matter of fact, the proof of correctness of the methods to optimise simulation scripts basically relies on an intuitive semantics for simulation scripting languages. This hampers the possibility of formally showing that the optimisations introduced to speed up the simulation activity do not actually omit checking of relevant behaviours for the system under verification. The aim of this paper is to fill the above gap by presenting an operational semantics for simulation scripting languages and by proving soundness and completeness properties for it. This, in turn, enables formal proofs of equivalence between unoptimised and optimised simulation scripts. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
2352-2208 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
MCLab @ davi @ Mancini2021100640 |
Serial |
183 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
|
|
Title |
An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks |
Type |
Conference Article |
|
Year |
2018 |
Publication |
Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
302-312 |
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
Best Paper |
Approved |
no |
|
|
Call Number |
MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 |
Serial |
176 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
|
|
Title |
Parallel Statistical Model Checking for Safety Verification in Smart Grids |
Type |
Conference Article |
|
Year |
2018 |
Publication |
2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
1-6 |
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
MCLab @ davi @ mancini-etal:2018:smartgridcomm |
Serial |
170 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.K.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
|
|
Title |
User Flexibility Aware Price Policy Synthesis for Smart Grids |
Type |
Conference Article |
|
Year |
2015 |
Publication |
Digital System Design (DSD), 2015 Euromicro Conference on |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
478-485 |
|
|
Keywords |
Contracts; Current measurement; Load management; Power demand; Power measurement; State estimation; Substations; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis |
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
Sapienza @ preissler @ Mancini_etal2015_3 |
Serial |
136 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Massini, A.; Tronci, E. |
|
|
Title |
Parallelization of Cycle-Based Logic Simulation |
Type |
Journal Article |
|
Year |
2017 |
Publication |
Parallel Processing Letters |
Abbreviated Journal |
|
|
|
Volume |
27 |
Issue |
02 |
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
MCLab @ davi @ |
Serial |
166 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Melatti, I.; Tronci, E. |
|
|
Title |
Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification |
Type |
Journal Article |
|
Year |
2021 |
Publication |
IEEE Transactions on Software Engineering |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
1-1 |
|
|
Keywords |
|
|
|
Abstract |
Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
1939-3520 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
To appear |
Approved |
no |
|
|
Call Number |
MCLab @ davi @ ref9527998 |
Serial |
191 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Tronci, E.; Scialanca, A.; Lanciotti, F.; Finzi, A.; Guarneri, R.; Di Pompeo, S. |
|
|
Title |
Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network |
Type |
Conference Article |
|
Year |
2018 |
Publication |
25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
MCLab @ davi @ |
Serial |
174 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, Toni ; Mari, Federico ; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
|
|
Title |
System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation |
Type |
Conference Article |
|
Year |
2014 |
Publication |
Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing |
Abbreviated Journal |
Euromicro International Conference on Parallel, Distributed and Network-Based Processing |
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
IEEE Computer Society |
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
Sapienza @ melatti @ |
Serial |
118 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico |
|
|
Title |
System Level Formal Verification via Model Checking Driven Simulation |
Type |
Conference Article |
|
Year |
2013 |
Publication |
Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia |
Abbreviated Journal |
CAV 2013 |
|
|
Volume |
|
Issue |
|
Pages |
296-312 |
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
|
Series Volume |
8044 |
Series Issue |
|
Edition |
|
|
|
ISSN |
0302-9743 |
ISBN |
978-3-642-39798-1 |
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ |
Serial |
113 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
|
|
Title |
Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation |
Type |
Conference Article |
|
Year |
2014 |
Publication |
In Proceedings of 17th EuroMicro Conference on Digital System Design (DSD 2014) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
|
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
MCLab @ davi @ |
Serial |
122 |
|
Permanent link to this record |