|
|
Amedeo Cesta, Simone Fratini, Andrea Orlandini, Alberto Finzi, and Enrico Tronci. "Flexible Plan Verification: Feasibility Results." Fundamenta Informaticae 107, no. 2 (2011): 111–137. DOI: 10.3233/FI-2011-397.
|
|
|
|
T. Mancini. "Now or Never: Negotiating Efficiently with Unknown or Untrusted Counterparts." Fundamenta Informaticae 149, no. 1-2 (2016): 61–100. DOI: 10.3233/FI-2016-1443.
|
|
|
|
T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. "SyLVaaS: System Level Formal Verification as a Service." Fundamenta Informaticae 149, no. 1-2 (2016): 101–132. DOI: 10.3233/FI-2016-1444.
|
|
|
|
Giuseppe Della Penna, Antinisca Di Marco, Benedetto Intrigila, Igor Melatti, and Alfonso Pierantonio. "Xere: Towards a Natural Interoperability between XML and ER Diagrams." In Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, edited by M. Pezzè, 356–371. Lecture Notes in Computer Science 2621. Springer, 2003. ISSN: 3-540-00899-3. DOI: 10.1007/3-540-36578-8_25.
Abstract: XML (eXtensible Markup Language) is becoming the standard format for documents on Internet and is widely used to exchange data. Often, the relevant information contained in XML documents needs to be also stored in legacy databases (DB) in order to integrate the new data with the pre-existing ones. In this paper, we introduce a technique for the automatic XML-DB integration, which we call Xere. In particular we present, as the first step of Xere, the mapping algorithm which allows the translation of XML Schemas into Entity-Relationship diagrams.
|
|
|
|
Michele Cecconi, and Enrico Tronci. "Requirements Formalization and Validation for a Telecommunication Equipment Protection Switcher." In Hase. IEEE Computer Society, 2000. ISSN: 0-7695-0927-4. DOI: 10.1109/HASE.2000.895456.
|
|
|
|
G. Dipoppa, G. D'Alessandro, R. Semprini, and E. Tronci. "Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design." In High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on, 209–219. Albuquerque, NM, USA: IEEE Computer Society, 2001. ISSN: 0-7695-1275-5. DOI: 10.1109/HASE.2001.966821.
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.
|
|
|
|
B. Leeners, T. Krueger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. Roeblitz, D. Wunder, L. Saleh et al. "Cognitive function in association with high estradiol levels resulting from fertility treatment." Hormones and Behavior 130 (2021): 104951. ISSN: 0018-506x. DOI: 10.1016/j.yhbeh.2021.104951.
Abstract: The putative association between hormones and cognitive performance is controversial. While there is evidence that estradiol plays a neuroprotective role, hormone treatment has not been shown to improve cognitive performance. Current research is flawed by the evaluation of combined hormonal effects throughout the menstrual cycle or in the menopausal transition. The stimulation phase of a fertility treatment offers a unique model to study the effect of estradiol on cognitive function. This quasi-experimental observational study is based on data from 44 women receiving IVF in Zurich, Switzerland. We assessed visuospatial working memory, attention, cognitive bias, and hormone levels at the beginning and at the end of the stimulation phase of ovarian superstimulation as part of a fertility treatment. In addition to inter-individual differences, we examined intra-individual change over time (within-subject effects). The substantial increases in estradiol levels resulting from fertility treatment did not relate to any considerable change in cognitive functioning. As the tests applied represent a broad variety of cognitive functions on different levels of complexity and with various brain regions involved, we can conclude that estradiol does not show a significant short-term effect on cognitive function.
Keywords: Cognition, Estrogen, Estradiol, Fertility treatment, Attention, Cognitive bias
|
|
|
|
Federico Mari, and Enrico Tronci. "CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems." In Hybrid Systems: Computation and Control (HSCC 2007), edited by A. Bemporad, A. Bicchi and G. C. Buttazzo, 399–412. Lecture Notes in Computer Science 4416. Springer, 2007. DOI: 10.1007/978-3-540-71493-4_32.
Abstract: Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
Keywords: Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS
|
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Michele Minichino, Ester Ciancamerla, Andrea Parisse, Enrico Tronci, and Marisa Venturini Zilli. "Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier." In Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings, edited by O. Maler and A. Pnueli, 141–155. Lecture Notes in Computer Science 2623. Springer, 2003. ISSN: 3-540-00913-2. DOI: 10.1007/3-540-36580-X.
Abstract: Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas.
|
|
|
|
Giuseppe Della Penna, Daniele Magazzeni, Alberto Tofani, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "Automatic Synthesis of Robust Numerical Controllers." In Icas '07, 4. IEEE Computer Society, 2007. ISSN: 0-7695-2859-5. DOI: 10.1109/CONIELECOMP.2007.59.
Abstract: A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the well-known CMurphi verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem.
|
|
