Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Merging Planning, Scheduling & Verification – A Preliminary Analysis." In In Proc. of 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA)., 2008.
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Validation and Verification Issues in a Timeline-based Planning System." In In E-Proc. of ICAPS Workshop on Knowledge Engineering for Planning and Scheduling., 2008.
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.
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Validation and verification issues in a timeline-based planning system." The Knowledge Engineering Review 25, no. 03 (2010): 299–318. Cambridge University Press. DOI: 10.1017/S0269888910000160.
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.
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Flexible Timeline-Based Plan Verification." In KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings, edited by B. Ã. ¤rbel Mertsching, M. Hund and M. Z. Aziz, 49–56. Lecture Notes in Computer Science 5803. Springer, 2009. ISSN: 978-3-642-04616-2. DOI: 10.1007/978-3-642-04617-9_7.
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Flexible Plan Verification: Feasibility Results." In 16th RCRA International Workshop on “Experimental evaluation of algorithms for solving problems with combinatorial explosion” (RCRA). Proceedings., 2009.
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Verifying Flexible Timeline-based Plans." In E-Proc. of ICAPS Workshop on Validation and Verification of Planning and Scheduling Systems., 2009.
Abstract: The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verification method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study.
|
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.
|
Federico Cavaliere, Federico Mari, Igor Melatti, Giovanni Minei, Ivano Salvo, Enrico Tronci, Giovanni Verzino, and Yuri Yushtein. "Model Checking Satellite Operational Procedures." In DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace., 2011.
Abstract: We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.
|
Edoardo Campagnano, Ester Ciancamerla, Michele Minichino, and Enrico Tronci. "Automatic Analysis of a Safety Critical Tele Control System." In 24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP), edited by R. Winther, B. A. Gran and G. Dahll, 94–107. Lecture Notes in Computer Science 3688. Fredrikstad, Norway: Springer, 2005. ISSN: 3-540-29200-4. DOI: 10.1007/11563228_8.
Abstract: We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.
|
Antonio Bucciarelli, and Ivano Salvo. "Totality, Definability and Boolean Circuits." 1443 (1998): 808–819. Springer. DOI: 10.1007/BFb0055104.
Abstract: In the type frame originating from the flat domain of boolean values, we single out elements which are hereditarily total. We show that these elements can be defined, up to total equivalence, by sequential programs. The elements of an equivalence class of the totality equivalence relation (totality class) can be seen as different algorithms for computing a given set-theoretic boolean function. We show that the bottom element of a totality class, which is sequential, corresponds to the most eager algorithm, and the top to the laziest one. Finally we suggest a link between size of totality classes and a well known measure of complexity of boolean functions, namely their sensitivity.
|