Home << 1 2 3 4 5 6 7 8 9 10 >> [11–15]
List View
 | 
Citations
 | 
Details
   web
Records
Author Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele
Title Fluid Petri Nets and hybrid model checking: a comparative case study Type Journal Article
Year 2003 Publication (up) Int. Journal on: Reliability Engineering & System Safety Abbreviated Journal
Volume 81 Issue 3 Pages 239-257
Keywords
Abstract The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a ’real world’ hybrid system: the temperature control system of a co-generative plant.
Address
Corporate Author Thesis
Publisher Elsevier 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 @ ress03 Serial 40
Permanent link to this record
 
 
Author Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico
Title Automated analysis of timed security: a case study on web privacy Type Journal Article
Year 2004 Publication (up) International Journal of Information Security Abbreviated Journal
Volume 2 Issue 3-4 Pages 168-186
Keywords
Abstract This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given.
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 yes
Call Number Sapienza @ mari @ ijis04 Serial 33
Permanent link to this record
 
 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Synthesizing Control Software from Boolean Relations Type Journal Article
Year 2012 Publication (up) International Journal on Advances in Software Abbreviated Journal Intern. Journal on Advances in SW
Volume vol. 5, nr 3&4 Issue Pages 212-223
Keywords Control Software Synthesis; Embedded Systems; Model Checking
Abstract Many software as well digital hardware automatic
synthesis methods define the set of
implementations meeting the given system
specifications with a boolean relation K. In
such a context a fundamental step in the software
(hardware) synthesis process is finding effective
solutions to the functional equation defined by
K. This entails finding a (set of) boolean
function(s) F (typically represented using
OBDDs, Ordered Binary Decision Diagrams)
such that: 1) for all x for which K is
satisfiable, K(x, F(x)) = 1 holds; 2) the
implementation of F is efficient with respect
to given implementation parameters such as code
size or execution time. While this problem has
been widely studied in digital hardware synthesis,
little has been done in a software synthesis
context. Unfortunately, the approaches developed
for hardware synthesis cannot be directly used in
a software context. This motivates investigation
of effective methods to solve the above problem
when F has to be implemented with software. In
this paper, we present an algorithm that, from an
OBDD representation for K, generates a C code
implementation for F that has the same size as
the OBDD for F and a worst case execution time
linear in nr, being n = |x| the number of
input arguments for functions in F and r the
number of functions in F. Moreover, a formal
proof of the proposed algorithm correctness is
also shown. Finally, we present experimental
results showing effectiveness of the proposed
algorithm.
Address
Corporate Author Thesis
Publisher IARIA Place of Publication Editor Luigi Lavazza
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1942-2628 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ melatti @ Serial 108
Permanent link to this record
 
 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems Type Journal Article
Year 2013 Publication (up) International Journal on Advances in Software Abbreviated Journal Intern. Journal on Advances in SW
Volume vol. 6, nr 1&2 Issue Pages 155-169
Keywords Model-based software design; Linear predicates; Hybrid systems
Abstract Model based design is particularly appealing in
software based control systems (e.g., embedded
software) design, since in such a case system
level specifications are much easier to define
than the control software behavior itself. In
turn, model based design of embedded systems
requires modeling both continuous subsystems
(typically, the plant) as well as discrete
subsystems (the controller). This is typically
done using hybrid systems. Mixed Integer Linear
Programming (MILP) based abstraction techniques
have been successfully applied to automatically
synthesize correct-by-construction control
software for discrete time linear hybrid systems,
where plant dynamics is modeled as a linear
predicate over state, input, and next state
variables. Unfortunately, MILP solvers require
such linear predicates to be conjunctions of
linear constraints, which is not a natural way of
modeling hybrid systems. In this paper we show
that, under the hypothesis that each variable
ranges over a bounded interval, any linear
predicate built upon conjunction and disjunction
of linear constraints can be automatically
translated into an equivalent conjunctive
predicate. Since variable bounds play a key role
in this translation, our algorithm includes a
procedure to compute all implicit variable bounds
of the given linear predicate. Furthermore, we
show that a particular form of linear predicates,
namely guarded predicates, are a natural and
powerful language to succinctly model discrete
time linear hybrid systems dynamics. Finally, we
experimentally show the feasibility of our
approach on an important and challenging case
study taken from the literature, namely the
multi-input Buck DC-DC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6-inputs Buck DC-DC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes.
Address
Corporate Author Thesis
Publisher IARIA Place of Publication Editor Luigi Lavazza
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1942-2628 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ melatti @ Serial 115
Permanent link to this record
 
 
Author Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti
Title Computing Biological Model Parameters by Parallel Statistical Model Checking Type Journal Article
Year 2015 Publication (up) International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) Abbreviated Journal
Volume 9044 Issue Pages 542-554
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 124
Permanent link to this record
 
 
Author Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico
Title A Symbolic Model Checker for ACTL Type Conference Article
Year 1998 Publication (up) International Workshop on Current Trends in Applied Formal Method (FM-Trends) Abbreviated Journal
Volume Issue Pages 228-242
Keywords
Abstract We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).
Address
Corporate Author Thesis
Publisher Springer Place of Publication Boppard, Germany Editor Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 1641 Series Issue Edition
ISSN 3-540-66462-9 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ fm-trends98 Serial 51
Permanent link to this record
 
 
Author Tronci, Enrico
Title Defining Data Structures via Böhm-Out Type Journal Article
Year 1995 Publication (up) J. Funct. Program. Abbreviated Journal
Volume 5 Issue 1 Pages 51-64
Keywords
Abstract We show that any recursively enumerable subset of a data structure can be regarded as the solution set to a B??hm-out problem.
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 yes
Call Number Sapienza @ mari @ jfp95 Serial 57
Permanent link to this record
 
 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title On Checking Equivalence of Simulation Scripts Type Journal Article
Year 2021 Publication (up) 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 Hengartner, M. P.; Kruger, T. H. C.; Geraedts, K.; Tronci, E.; Mancini, T.; Ille, F.; Egli, M.; Röblitz, S.; Ehrig, R.; Saleh, L.; Spanaus, K.; Schippert, C.; Zhang, Y.; Leeners, B.
Title Negative affect is unrelated to fluctuations in hormone levels across the menstrual cycle: Evidence from a multisite observational study across two successive cycles Type Journal Article
Year 2017 Publication (up) Journal of Psychosomatic Research Abbreviated Journal
Volume 99 Issue Pages 21-27
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 165
Permanent link to this record
 
 
Author Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
Title Flexible Timeline-Based Plan Verification Type Conference Article
Year 2009 Publication (up) KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings Abbreviated Journal
Volume Issue Pages 49-56
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Mertsching, Bärbel; Hund, M.; Aziz, M.Z.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 5803 Series Issue Edition
ISSN 978-3-642-04616-2 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Cffot09 Serial 21
Permanent link to this record