| |
Records |
Links |
|
Author |
Tronci, Enrico |
|
| |
Title |
Automatic Synthesis of Control Software for an Industrial Automation Control System |
Type |
Conference Article |
| |
Year |
1999 |
Publication |
Proc.of: 14th IEEE International Conference on: Automated Software Engineering (ASE) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
247-250 |
|
| |
Keywords |
|
|
| |
Abstract |
We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design, followed by automatic verification. Our experimental results show that for industrial automation control systems, automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design, followed by automatic verification. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
Place of Publication |
Cocoa Beach, Florida, USA |
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 @ ase99 |
Serial |
49 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe |
|
| |
Title |
Disk Based Software Verification via Bounded Model Checking |
Type |
Conference Article |
| |
Year |
2007 |
Publication |
APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
358-365 |
|
| |
Keywords |
|
|
| |
Abstract |
One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
0-7695-3057-5 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Bmtd07 |
Serial |
76 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa |
|
| |
Title |
A Probabilistic Approach to Automatic Verification of Concurrent Systems |
Type |
Conference Article |
| |
Year |
2001 |
Publication |
8th Asia-Pacific Software Engineering Conference (APSEC) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
317-324 |
|
| |
Keywords |
|
|
| |
Abstract |
The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead it just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that by using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Computer Society |
Place of Publication |
Macau, China |
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
0-7695-1408-1 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ apsec01 |
Serial |
43 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Maggioli, F.; Mancini, T.; Tronci, E. |
|
| |
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 |
| |
|
| |
|
Author |
Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Leeners, B. |
|
| |
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 |
Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano |
|
| |
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 |
Tronci, Enrico |
|
| |
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 |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
|
| |
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 |
Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano |
|
| |
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 |
Focardi, Riccardo; Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico |
|
| |
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 |
