Enabling On-Board Autonomy: a Platform for the Development of Verified Software

ASI - DOVES DIT-PRJ-02-022

Status NOT active project
DISI role Partner
Project type Research Project
Dimension National
Acquisition date 2002-11-15
Start date 2002-11-15
End date 2004-11-15
SAP code 40100511

Project details

Project astract This project aims at delivering effective methods and tools for enabling the production of verified Autonomous On-board Software (AOS). The objective will be achieved by means of two parallel and tightly integrated activities:<br/>- The investigation on advanced V\&V and synthesis techniques for Autonomous On-board Software (AOS).<br/>- The design and the implementation of a platform for the advanced support of the development of AOS.<br/>
Fundings 192868 €
Partners
  • SRA - ITC IRST
  • DIST - Università di Genova
  • DIS - Università di Roma I
  • DIT - University of Trento
  • DIST - Universit
  • DIS - Universit

DISI Sub-project details

Project astract Binary Decision Diagrams (BDDs) and related<br/>techniques forms the backbone of most current verification tools (Cadence by Cadence Inc, Thunder by Intel, etc.) and in particular the NuSMV checker which has been developed at IRST in collaboration with<br/>researchers at the Univ. of Trento. Within this<br/>work package we focus on synthesis methods for AOS.<br/>Two research directions have been foreseen.<br/><br/>The first direction concerns the extension of the BDD reasoning tools to the synthesis of AOS. The starting point is the planning-as-model-checking paradigm used for to classical AI planning, that will be lifted to AOS. This activity will also exploit some techniques developed for domains (e.g., security domains) where failures, concurrency, and an hostile environment play a key role.<br/><br/>The second, longer term research direction will build on the incorporation of arithmetical constraints into the BDD reasoning engine (see description of WP2). We will investigate the possibility of extending the planning-as-model-checking approach to this more<br/>expressive framework, thus allowing for the synthesis of AOS that satisfy performance guarantees that are best expressed by numerical constraints.
Fundings 20000 €
Manager Fabio Massacci