Home << 1 2 3 4 5 6 7 8 9 10 >> [11–15]
List View
 | 
Citations
 | 
Details
   web
Records
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title Anytime system level verification via parallel random exhaustive hardware in the loop simulation Type Journal Article
Year 2016 Publication (down) 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 Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano
Title Intersection types and λ-definability Type Journal Article
Year 2003 Publication (down) Mathematical Structures in Computer Science Abbreviated Journal
Volume 13 Issue 1 Pages 15-53
Keywords
Abstract This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
Address
Corporate Author Thesis
Publisher Cambridge University Press Place of Publication New York, NY, USA Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0960-1295 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03 Serial 69
Permanent link to this record
 
 
Author
Title Charme Type Conference Article
Year 2003 Publication (down) 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 Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
Title Flexible Timeline-Based Plan Verification Type Conference Article
Year 2009 Publication (down) 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
 
 
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 (down) 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 Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title On Checking Equivalence of Simulation Scripts Type Journal Article
Year 2021 Publication (down) 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 Tronci, Enrico
Title Defining Data Structures via Böhm-Out Type Journal Article
Year 1995 Publication (down) 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 Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico
Title A Symbolic Model Checker for ACTL Type Conference Article
Year 1998 Publication (down) 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 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 (down) 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 Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Synthesizing Control Software from Boolean Relations Type Journal Article
Year 2012 Publication (down) 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