toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele pdf  doi
openurl 
  Title Fluid Petri Nets and hybrid model checking: a comparative case study Type Journal Article
  Year 2003 Publication 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 Bono, V.; Salvo, I. pdf  url
doi  openurl
  Title A CuCh Interpretation of an Object-Oriented Language Type Journal Article
  Year 2001 Publication Electronic Notes in Theoretical Computer Science Abbreviated Journal  
  Volume 50 Issue 2 Pages 159-177  
  Keywords  
  Abstract CuCh machine extends pure lambda–calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of overloading to define a functional interpretation of a simple, but significant fragment of a typical object-oriented language.  
  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 BOTH 2001, Bohm’s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001) Approved yes  
  Call Number Sapienza @ mari @ Bono-Salvo:BOTH01 Serial 72  
Permanent link to this record
 

 
Author Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; Salvo, Ivano; Sassone, Vladimiro pdf  doi
openurl 
  Title A Type Inference Algorithm for Secure Ambients Type Journal Article
  Year 2002 Publication Electronic Notes in Theoretical Computer Science Abbreviated Journal  
  Volume 62 Issue Pages 83-101  
  Keywords  
  Abstract We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario.  
  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 TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types Approved yes  
  Call Number Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01 Serial 73  
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 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 Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano pdf  doi
openurl 
  Title Mobility Types for Mobile Processes in Mobile Ambients Type Journal Article
  Year 2003 Publication Electr. Notes Theor. Comput. Sci. Abbreviated Journal  
  Volume 78 Issue Pages  
  Keywords  
  Abstract We present an ambient-like calculus in which the open capability is dropped, and a new form of “lightweight†process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the “minimal†requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way.  
  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 @ Coppo-Dezani-Giovannetti-Salvo:03 Serial 74  
Permanent link to this record
 

 
Author Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico pdf  doi
openurl 
  Title Validation and verification issues in a timeline-based planning system Type Journal Article
  Year 2010 Publication The Knowledge Engineering Review Abbreviated Journal  
  Volume 25 Issue 03 Pages 299-318  
  Keywords  
  Abstract One of the key points to take into account to foster effective introduction of AI planning and scheduling systems in real world is to develop end user trust in the related technologies. Automated planning and scheduling systems often brings solutions to the users which are neither “obvious†nor immediately acceptable for them. This is due to the ability of these tools to take into account quite an amount of temporal and causal constraints and to employ resolution processes often designed to optimize the solution with respect to non trivial evaluation functions. To increase technology trust, the study of tools for verifying and validating plans and schedules produced by AI systems might be instrumental. In general, validation and verification techniques represent a needed complementary technology in developing domain independent architectures for automated problem solving. This paper presents a preliminary report of the issues concerned with the use of two software tools for formal verification of finite state systems to the validation of the solutions produced by MrSPOCK, a recent effort for building a timeline based planning tool in an ESA project.  
  Address  
  Corporate Author Thesis  
  Publisher Cambridge University Press 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 @ Cffot10 Serial 18  
Permanent link to this record
 

 
Author Tronci, Enrico doi  openurl
  Title Defining Data Structures via Böhm-Out Type Journal Article
  Year 1995 Publication 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 Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano file  doi
openurl 
  Title Intersection types and λ-definability Type Journal Article
  Year 2003 Publication 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 Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Leeners, B. pdf  url
doi  openurl
  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
 

 
Author Maggioli, F.; Mancini, T.; Tronci, E. pdf  url
doi  openurl
  Title SBML2Modelica: Integrating biochemical models within open-standard simulation ecosystems Type Journal Article
  Year 2019 Publication Bioinformatics Abbreviated Journal  
  Volume 36 Issue 7 Pages 2165–2172  
  Keywords  
  Abstract SBML is the most widespread language for the definition of biochemical models. Although dozens of SBML simulators are available, there is a general lack of support to the integration of SBML models within open-standard general-purpose simulation ecosystems. This hinders co-simulation and integration of SBML models within larger model networks, in order to, e.g., enable in-silico clinical trials of drugs, pharmacological protocols, or engineering artefacts such as biomedical devices against Virtual Physiological Human models.Modelica is one of the most popular existing open-standard general-purpose simulation languages, supported by many simulators. Modelica models are especially suited for the definition of complex networks of heterogeneous models from virtually all application domains. Models written in Modelica (and in 100+ other languages) can be readily exported into black-box Functional Mock-Up Units (FMUs), and seamlessly co-simulated and integrated into larger model networks within open-standard language-independent simulation ecosystems.In order to enable SBML model integration within heterogeneous model networks, we present SBML2Modelica, a software system translating SBML models into well-structured, user-intelligible, easily modifiable Modelica models. SBML2Modelica is SBML Level 3 Version 2 -compliant and succeeds on 96.47% of the SBML Test Suite Core (with a few rare, intricate, and easily avoidable combinations of constructs unsupported and cleanly signalled to the user). Our experimental campaign on 613 models from the BioModels database (with up to 5438 variables) shows that the major open-source (general-purpose) Modelica and FMU simulators achieve performance comparable to state-of-the-art specialised SBML simulators.SBML2Modelica is written in Java and is freely available for non-commercial use at https://bitbucket.org/mclab/sbml2modelica  
  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/btz860 Serial 179  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: