|
Records |
Links ![sorted by URL field, ascending order (up)](img/sort_asc.gif) |
|
Author |
Driouich, Y.; Parente, M.; Tronci, E. |
![goto web page (via DOI) doi](img/doi.gif)
|
|
Title |
Modeling cyber-physical systems for automatic verification |
Type |
Conference Article |
|
Year |
2017 |
Publication |
14th International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design (SMACD 2017) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
1-4 |
|
|
Keywords |
cyber-physical systems;formal verification;maximum power point trackers;power engineering computing;Modelica;automatic verification;complex power electronics systems;cyber-physical systems modeling;distributed maximum power point tracking system;open standard modeling language;Computational modeling;Control systems;Integrated circuit modeling;Mathematical model;Maximum power point trackers;Object oriented modeling;Radiation effects;Automatic Formal Verification;Cyber-Physical Systems;DMPPT;Modeling;Photovoltaic systems;Simulation;System Analysis and Design |
|
|
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 @ ref7981621 |
Serial |
168 |
|
Permanent link to this record |
|
|
|
|
Author |
Driouich, Y.; Parente, M.; Tronci, E. |
![goto web page (via DOI) doi](img/doi.gif)
|
|
Title |
Model Checking Cyber-Physical Energy Systems |
Type |
Conference Article |
|
Year |
2018 |
Publication |
Proceedings of 2017 International Renewable and Sustainable Energy Conference, IRSEC 2017 |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Institute of Electrical and Electronics Engineers Inc. |
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 @ Driouich2018 |
Serial |
177 |
|
Permanent link to this record |
|
|
|
|
Author |
Driouich, Y.; Parente, M.; Tronci, E. |
![goto web page (via DOI) doi](img/doi.gif)
|
|
Title |
A methodology for a complete simulation of Cyber-Physical Energy Systems |
Type |
Conference Article |
|
Year |
2018 |
Publication |
EESMS 2018 – Environmental, Energy, and Structural Monitoring Systems, Proceedings |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
1-5 |
|
|
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 @ Driouich20181 |
Serial |
169 |
|
Permanent link to this record |
|
|
|
|
Author |
|
![goto web page (via DOI) doi](img/doi.gif)
|
|
Title |
Charme |
Type |
Conference Article |
|
Year |
2003 |
Publication |
Lecture Notes in Computer Science |
Abbreviated Journal |
|
|
|
Volume |
2860 |
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer |
Place of Publication |
|
Editor |
Geist, D.; Tronci, E. |
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ editor-charme03 |
Serial |
37 |
|
Permanent link to this record |
|
|
|
|
Author |
Martinelli, Marco; Tronci, Enrico; Dipoppa, Giovanni; Balducelli, Claudio |
![goto web page (via DOI) doi](img/doi.gif)
|
|
Title |
Electric Power System Anomaly Detection Using Neural Networks |
Type |
Conference Article |
|
Year |
2004 |
Publication |
8th International Conference on: Knowledge-Based Intelligent Information and Engineering Systems (KES) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
1242-1248 |
|
|
Keywords |
|
|
|
Abstract |
The aim of this work is to propose an approach to monitor and protect Electric Power System by learning normal system behaviour at substations level, and raising an alarm signal when an abnormal status is detected; the problem is addressed by the use of autoassociative neural networks, reading substation measures. Experimental results show that, through the proposed approach, neural networks can be used to learn parameters underlaying system behaviour, and their output processed to detecting anomalies due to hijacking of measures, changes in the power network topology (i.e. transmission lines breaking) and unexpected power demand trend. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer |
Place of Publication |
Wellington, New Zealand |
Editor |
Negoita, M.G.; Howlett, R.J.; Jain, L.C. |
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
|
Series Volume |
3213 |
Series Issue |
|
Edition |
|
|
|
ISSN |
3-540-23318-0 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ kes04 |
Serial |
35 |
|
Permanent link to this record |
|
|
|
|
Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
![goto web page url](img/www.gif)
|
|
Title |
A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software |
Type |
Report |
|
Year |
2012 |
Publication |
|
Abbreviated Journal |
|
|
|
Volume |
abs/1210.2276 |
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
Many Control Systems are indeed Software Based Control Systems, i.e. control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of control software.
Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis.
In this paper, we present a map-reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis.
We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 65%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm in QKS. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
CoRR, Technical Report |
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 |
yes |
|
|
Call Number |
Sapienza @ mari @ |
Serial |
101 |
|
Permanent link to this record |
|
|
|
|
Author |
Tronci, Enrico |
![goto web page url](img/www.gif)
![find record details (via OpenURL) openurl](img/xref.gif)
|
|
Title |
Optimal Finite State Supervisory Control |
Type |
Conference Article |
|
Year |
1996 |
Publication |
CDC '96: Proceedings of the 35th IEEE International Conference on Decision and Control |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
Supervisory Controllers are Discrete Event Dynamic Systems (DEDSs) forming the discrete core of a Hybrid Control System. We address the problem of automatic synthesis of Optimal Finite State Supervisory Controllers (OSCs). We show that Boolean First Order Logic (BFOL) and Binary Decision Diagrams (BDDs) are an effective methodological and practical framework for Optimal Finite State Supervisory Control. Using BFOL programs (i.e. systems of boolean functional equations) and BDDs we give a symbolic (i.e. BDD based) algorithm for automatic synthesis of OSCs. Our OSC synthesis algorithm can handle arbitrary sets of final states as well as plant transition relations containing loops and uncontrollable events (e.g. failures). We report on experimental results on the use of our OSC synthesis algorithm to synthesize a C program implementing a minimum fuel OSC for two autonomous vehicles moving on a 4 x 4 grid. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
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 |
yes |
|
|
Call Number |
Sapienza @ mari @ cdc96 |
Serial |
67 |
|
Permanent link to this record |
|
|
|
|
Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
![goto web page url](img/www.gif)
![find record details (via OpenURL) openurl](img/xref.gif)
|
|
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. |
![goto web page url](img/www.gif)
![find record details (via OpenURL) openurl](img/xref.gif)
|
|
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 |
Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Leeners, B. |
![goto web page url](img/www.gif)
![find record details (via OpenURL) openurl](img/xref.gif)
|
|
Title |
Complete populations of virtual patients for in silico clinical trials |
Type |
Journal Article |
|
Year |
2021 |
Publication |
Bioinformatics |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
1-8 |
|
|
Keywords |
|
|
|
Abstract |
Model-based approaches to safety and efficacy assessment of pharmacological drugs, treatment strategies, or medical devices (In Silico Clinical Trial, ISCT) aim to decrease time and cost for the needed experimentations, reduce animal and human testing, and enable precision medicine. Unfortunately, in presence of non-identifiable models (e.g., reaction networks), parameter estimation is not enough to generate complete populations of Virtual Patient (VPs), i.e., populations guaranteed to show the entire spectrum of model behaviours (phenotypes), thus ensuring representativeness of the trial.We present methods and software based on global search driven by statistical model checking that, starting from a (non-identifiable) quantitative model of the human physiology (plus drugs PK/PD) and suitable biological and medical knowledge elicited from experts, compute a population of VPs whose behaviours are representative of the whole spectrum of phenotypes entailed by the model (completeness) and pairwise distinguishable according to user-provided criteria. This enables full granularity control on the size of the population to employ in an ISCT, guaranteeing representativeness while avoiding over-representation of behaviours.We proved the effectiveness of our algorithm on a non-identifiable ODE-based model of the female Hypothalamic-Pituitary-Gonadal axis, by generating a population of 4 830 264 VPs stratified into 7 levels (at different granularity of behaviours), and assessed its representativeness against 86 retrospective health records from Pfizer, Hannover Medical School and University Hospital of Lausanne. The datasets are respectively covered by our VPs within Average Normalised Mean Absolute Error of 15%, 20%, and 35% (90% of the latter dataset is covered within 20% error). |
|
|
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 |
1367-4803 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
no |
|
|
Call Number |
MCLab @ davi @ ref10.1093/bioinformatics/btaa1026 |
Serial |
182 |
|
Permanent link to this record |