toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links (down)
Author Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. pdf  url
doi  openurl
  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 Ehrig, R.; Dierkes, T.; Schaefer, S.; Roeblitz, S.; Tronci, E.; Mancini, T.; Salvo, I.; Alimguzhin, V.; Mari, F.; Melatti, I.; Massini, A.; Leeners, B.; Krueger, T.H.C.; Egli, M.; Ille, F. pdf  url
doi  openurl
  Title An integrative approach for model driven computation of treatments in reproductive medicine Type Conference Article
  Year 2015 Publication Proceedings of the 15th International Symposium on Mathematical and Computational Biology (BIOMAT 2015), Rorkee, India 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 Sapienza @ preissler @ Ehrig_etal2015 Serial 144  
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico pdf  url
openurl 
  Title Synthesizing Control Software from Boolean Relations Type Journal Article
  Year 2012 Publication 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 pdf  url
openurl 
  Title From Boolean Relations to Control Software Type Conference Article
  Year 2011 Publication Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances Abbreviated Journal  
  Volume Issue Pages 528-533  
  Keywords  
  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 WCET (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.  
  Address  
  Corporate Author Thesis  
  Publisher ThinkMind Place of Publication Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 978-1-61208-165-6 ISBN Medium  
  Area Expedition Conference  
  Notes Best Paper Award Approved yes  
  Call Number Sapienza @ mari @ icsea11 Serial 14  
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. pdf  url
doi  openurl
  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 Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa pdf  url
openurl 
  Title Synchronized Regular Expressions Type Journal Article
  Year 2002 Publication Electr. Notes Theor. Comput. Sci. Abbreviated Journal  
  Volume 62 Issue Pages 195-210  
  Keywords  
  Abstract Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday stresses the need of more powerful tools to interact with texts. Indeed, much work has been done to provide nonprogramming tools that can be useful for the most common text manipulation issues. Regular Expressions (RE), introduced by Kleene, are well–known in the formal language theory. RE received several extensions, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [A] UNIX command, or the Perl [17] language pattern matching constructs) we find backreferences (as defind in [1]), i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all the kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. Therefore, we introduce the Synchronized Regular Expressions (SRE) as a derivation of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are talking about formalisms that should have a practical utility and can be used in the real world, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user–friendly syntax for SRE to be used in implementations of SRE–powered search algorithms.  
  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 TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types Approved yes  
  Call Number Sapienza @ mari @ entcs02 Serial 46  
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. pdf  url
doi  openurl
  Title Anytime system level verification via parallel random exhaustive hardware in the loop simulation Type Journal Article
  Year 2016 Publication Microprocessors and Microsystems Abbreviated Journal  
  Volume 41 Issue Pages 12-28  
  Keywords Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation  
  Abstract Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.  
  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 0141-9331 ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number MCLab @ davi @ Mancini201612 Serial 155  
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico pdf  url
openurl 
  Title Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems Type Journal Article
  Year 2013 Publication 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 Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto pdf  url
doi  openurl
  Title A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET Type Journal Article
  Year 2013 Publication Mobile Information Systems Abbreviated Journal Mobile Information Systems  
  Volume 3 Issue 9 Pages 261-280  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher IOS Press Place of Publication Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 1574-017x (Print) 1875-905X (Online) ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ melatti @ Serial 109  
Permanent link to this record
 

 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico pdf  url
doi  openurl
  Title Simulator Semantics for System Level Formal Verification Type Conference Article
  Year 2015 Publication Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), 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 125  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: