toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Dipoppa, G.; D'Alessandro, G.; Semprini, R.; Tronci, E. pdf  doi
openurl 
  Title Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design Type Conference Article
  Year 2001 Publication High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on Abbreviated Journal  
  Volume Issue Pages (up) 209-219  
  Keywords  
  Abstract A railway interlocking system (RIS) is an embedded system (namely a supervisory control system) that ensures the safe, operation of the devices in a railway station. RIS is a safety critical system. We explore the possibility of integrating automatic formal verification methods in a given industry RIS design flow. The main obstructions to be overcome in our work are: selecting a formal verification tool that is efficient enough to solve the verification problems at hand; and devising a cost effective integration strategy for such tool. We were able to devise a successful integration strategy meeting the above constraints without requiring major modification in the pre-existent design flow nor retraining of personnel. We run verification experiments for a RIS designed for the Singapore Subway. The experiments show that the RIS design flow obtained from our integration strategy is able to automatically verify real life RIS designs.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication Albuquerque, NM, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0-7695-1275-5 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ hase01 Serial 45  
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 (up) 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 Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa pdf  doi
openurl 
  Title Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier Type Conference Article
  Year 2004 Publication Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings Abbreviated Journal  
  Volume Issue Pages (up) 214-229  
  Keywords  
  Abstract In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Hu, A.J.; Martin, A.K.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 3312 Series Issue Edition  
  ISSN 3-540-23738-0 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Dimtz04 Serial 87  
Permanent link to this record
 

 
Author Tortora, L.; Meynen, G.; Bijlsma, J.; Tronci, E.; Ferracuti, S. pdf  url
doi  openurl
  Title Neuroprediction and A.I. in Forensic Psychiatry and Criminal Justice: A Neurolaw Perspective Type Journal Article
  Year 2020 Publication Frontiers in Psychology Abbreviated Journal  
  Volume 11 Issue Pages (up) 220  
  Keywords  
  Abstract Advances in the use of neuroimaging in combination with A.I., and specifically the use of machine learning techniques, have led to the development of brain-reading technologies which, in the nearby future, could have many applications, such as lie detection, neuromarketing or brain-computer interfaces. Some of these could, in principle, also be used in forensic psychiatry. The application of these methods in forensic psychiatry could, for instance, be helpful to increase the accuracy of risk assessment and to identify possible interventions. This technique could be referred to as ‘A.I. neuroprediction,Â’ and involves identifying potential neurocognitive markers for the prediction of recidivism. However, the future implications of this technique and the role of neuroscience and A.I. in violence risk assessment remain to be established. In this paper, we review and analyze the literature concerning the use of brain-reading A.I. for neuroprediction of violence and rearrest to identify possibilities and challenges in the future use of these techniques in the fields of forensic psychiatry and criminal justice, considering legal implications and ethical issues. The analysis suggests that additional research is required on A.I. neuroprediction techniques, and there is still a great need to understand how they can be implemented in risk assessment in the field of forensic psychiatry. Besides the alluring potential of A.I. neuroprediction, we argue that its use in criminal justice and forensic psychiatry should be subjected to thorough harms/benefits analyses not only when these technologies will be fully available, but also while they are being researched and developed.  
  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 1664-1078 ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number MCLab @ davi @ Neuroprediction-2020 Serial 180  
Permanent link to this record
 

 
Author Alimguzhin, V.; Mari, F.; Melatti, I.; Tronci, E.; Ebeid, E.; Mikkelsen, S.A.; Jacobsen, R.H.; Gruber, J.K.; Hayes, B.; Huerta, F.; Prodanovic, M. pdf  doi
openurl 
  Title A Glimpse of SmartHG Project Test-bed and Communication Infrastructure Type Conference Article
  Year 2015 Publication Digital System Design (DSD), 2015 Euromicro Conference on Abbreviated Journal  
  Volume Issue Pages (up) 225-232  
  Keywords Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; 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 @ Alimguzhin_etal2015 Serial 127  
Permanent link to this record
 

 
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico pdf  doi
isbn  openurl
  Title On Model Based Synthesis of Embedded Control Software Type Conference Article
  Year 2012 Publication Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012 Abbreviated Journal  
  Volume Issue Pages (up) 227-236  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher ACM Place of Publication Editor Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN ISBN 978-1-4503-1425-1 Medium  
  Area Expedition Conference  
  Notes Techreport version can be found at arxiv.org Approved yes  
  Call Number Sapienza @ mari @ emsoft12 Serial 97  
Permanent link to this record
 

 
Author Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico pdf  doi
openurl 
  Title A Symbolic Model Checker for ACTL Type Conference Article
  Year 1998 Publication International Workshop on Current Trends in Applied Formal Method (FM-Trends) Abbreviated Journal  
  Volume Issue Pages (up) 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 Focardi, Riccardo; Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico pdf  doi
openurl 
  Title Formal Models of Timing Attacks on Web Privacy Type Journal Article
  Year 2002 Publication Electronic Notes in Theoretical Computer Science Abbreviated Journal  
  Volume 62 Issue Pages (up) 229-243  
  Keywords  
  Abstract We model a timing attack on web privacy proposed by Felten and Schneider by using three different approaches: HL-Timed Automata, SMV model checker, and tSPA Process Algebra. Some comparative analysis on the three approaches is derived.  
  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 @ entcs02a Serial 47  
Permanent link to this record
 

 
Author Chen, Q.M.; Finzi, A.; Mancini, T.; Melatti, I.; Tronci, E. pdf  doi
openurl 
  Title MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks Type Journal Article
  Year 2020 Publication Abbreviated Journal Fundamenta Informaticae  
  Volume 174 Issue Pages (up) 229-258  
  Keywords  
  Abstract In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes . As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance ). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.  
  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 1875-8681 ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number MCLab @ davi @ Serial 188  
Permanent link to this record
 

 
Author Intrigila, Benedetto; Melatti, Igor; Tofani, Alberto; Macchiarelli, Guido pdf  doi
openurl 
  Title Computational models of myocardial endomysial collagen arrangement Type Journal Article
  Year 2007 Publication Computer Methods and Programs in Biomedicine Abbreviated Journal  
  Volume 86 Issue 3 Pages (up) 232-244  
  Keywords  
  Abstract Collagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude /net extension is intended to model the stress /strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress /strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size.  
  Address  
  Corporate Author Thesis  
  Publisher Elsevier North-Holland, Inc. 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 0169-2607 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Imtm07 Serial 82  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: