Industrial Internet of Things (IIoT) systems require robust mechanisms for secure firmware updates. Existing approaches are often inadequate due to vendor fragmentation, network limitations, and the safety-critical nature of many IIoT applications. In this article, we address these challenges by extending the IETF SUIT (Software Updates for Internet of Things) framework to enhance the security and assurance of firmware updates. Our contributions include the integration of Software Bill of Materials (SBOM) mechanisms and a Behavioral Certification Manifest into the SUIT architecture to increase transparency and provide formal guarantees about the content of the update. The approach is validated by a prototype implementation that demonstrates its feasibility and scalability using real-world benchmarks.

Abstract In the field of formal verification, certifying proofs serve as compelling evidence to demonstrate the correctness of a model within a deductive system. These proofs can be automatically generated as a by-product of the verification process and are key artifacts for high-assurance systems. Their significance lies in their ability to be independently verified by proof checkers, which provides a more convenient approach than certifying the tools that generate them. Modern model checking algorithms adopt deductive methods and usually generate proofs in terms of inductive invariants, assuming that these apply to the original system under verification. Model checkers, though, often make use of a range of complex pre-processing simplifications and transformations to ease the verification process, which add another layer of complexity to the generation of proofs. In this paper, we present a novel approach for certifying model checking results exploiting a theorem prover and a theory of temporal deductive rules that can support various kinds of transformations and simplification of the original circuit. We implemented and experimentally evaluated our contribution on invariants generated using two state-of-the-art model checkers, nuXmv and PdTRAV, and by defining a set of rules within a theorem prover, to validate each certificate.

In this paper, we propose a robot oriented knowledge representation system based on the use of the Prolog language. Our framework hinges on a special organisation of Knowledge Base (KB) that enables: 1) its efficient population from natural language texts using semi-automated procedures based on Large Language Models (LLMs); 2) the seamless generation of temporal parallel plans for multi-robot systems through a sequence of transformations; 3) the automated translation of the plan into an executable formalism. The framework is supported by a set of open source tools and its functionality is shown with a realistic application.

Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (including planning, business process management, run-time monitoring, and reactive synthesis). Several studies have challenged the satisfiability problem thus far. In this paper, we focus instead on unsatisfiable LTLf specifications, with the objective of extracting the subset of formulae that cause inconsistencies within them, i.e., the unsatisfiable cores. We provide four algorithms to this end, which leverage the adaptation of a range of state-of-the-art algorithms to LTLf satisfiability checking. We implement those algorithms extending the respective implementations and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable specifications. The results put in evidence that the different algorithms and tools exhibit complementary features determining their efficiency and efficacy. Indeed, our findings suggest exploring different strategies and algorithmic solutions for the extraction of unsatisfiable cores from LTLf specifications, thus confirming the challenging and multi-faceted nature of this problem.

The high profitability of mining cryptocurrencies mining, a computationally intensive activity, forms a fertile ecosystem that is enticing not only legitimate investors but also cyber attackers who invest their illicit computational resources in this area. Cryptojacking refers to the surreptitious exploitation of a victim’s computing resources to mine cryptocurrencies on behalf of the cyber-criminal. This malicious behavior is observed in executable files and browser executable codes, including JavaScript and Assembly modules, downloaded from websites to victims’ machines and executed. Although there are numerous botnet detection techniques to stop this malicious activity, attackers can circumvent these protections using a variety of techniques. In this paper, CryptojackingTrap is presented as a novel cryptojacking detection solution designed to resist most malware defense methods. The CryptojackingTrap is armed with a debugger and extensible cryptocurrency listeners and its algorithm is based on the execution of cryptocurrency hash functions: an indispensable behavior of all cryptojacking executors. This algorithm becomes aware of this specific hash execution by correlating the memory access traces of suspicious executables with publicly available cryptocurrency P2P network data. With the advantage of this assembly-level investigation and a natureinspired approach to triggering the detection alarm, CryptojackingTrap provides an accurate, evasion-proof technique for detecting cryptojacking. After experimental evaluation, the false negative and false positive rates are zero, and in addition, the false positive rate is mathematically calculated as 10−20. CryptojackingTrap has an open, extensible architecture and is available to the open-source community.

Runtime attacks are a rising threat to both low- and high-end systems with the spread of techniques such as Return-Oriented Programming (ROP), which aims at hijacking the control flow of vulnerable applications. Although several control flow integrity schemes have been proposed by both academia and the industry, the vast majority of them are not compatible with low-end embedded devices, especially the ones that lack hardware security features. In this article, we propose \(\sf {\textsc {FLAShadow}}\) , a secure shadow stack design and implementation for low-end embedded systems, relying on zero hardware security features. The key idea is to leverage a software-based memory isolation mechanism to establish an integrity-protected memory area on the Flash of the target device, where \(\sf {\textsc {FLAShadow}}\) can be securely maintained. \(\sf {\textsc {FLAShadow}}\) exclusively reserves a register for maintaining the integrity of the stack pointer and also depends on a minimal trusted runtime component to avoid trusting the compiler toolchain. We evaluate an open-source implementation of \(\sf {\textsc {FLAShadow}}\) for the MSP430 architecture, showing an average performance and memory overhead of 168.58% and 25.91%, respectively. While the average performance overhead is considered high, we show that it is application dependent and incurs less than 5% for some applications.

Autonomous vehicle racing is facing a growing interest both in industrial and academic settings spanning multiple disciplines. In this paper, we will explore how to create a robust, efficient, and reliable decision-making mechanism to decide, at every point in time, the trajectories that a vehicle should take to overtake its opponents and win the race. The proposed framework combines a graph-based path planner with a game-theoretic model to generate powerful racing strategies. We implemented the framework, and we carried out an experimental evaluation to show its effectiveness and evaluate the impact of the different parameters.

Memory corruption vulnerabilities remain a prevalent threat on low-cost bare-metal devices. Fuzzing is a popular technique for automatically discovering such vulnerabilities. However, bare-metal devices lack even basic security mechanisms such as Memory Management Unit. Consequently, fuzzing approaches encounter silent memory corruptions with no visible effects, making even discovery difficult. Once discovered, it is also essential to identify the type of observed vulnerability for applying mitigation. Both discovery and identification remain open challenges in the case of fuzzing firmware binaries. This article addresses these problems by proposing an automated instrumentation technique that allows the observation of memory corruption vulnerabilities that are otherwise not observable and facilitates the automated identification of the observed vulnerability. Additionally, we surveyed state-of-the-art IoT fuzzers and analyzed their experimental methodologies. We found that existing approaches have fundamental problems that lead to incorrect or misleading results. To evaluate the effectiveness of IoT fuzzers, it is essential to determine the range and type of vulnerabilities that these fuzzers can discover. Thus, we propose the first ground-truth benchmark suite for IoT fuzzers that enables accurate and consistent evaluation of their vulnerability-finding performance. Our instrumentation framework's efficacy and efficiency in combination with state-of-the-art IoT fuzzers are assessed using the proposed benchmark.

The BDI model proved to be effective for the developing of applications requiring high-levels of autonomy and to deal with the complexity and unpredictability of real-world scenarios. The model, however, has significant limitations in reacting and handling contingencies within the given real-time constraints. Without an explicit representation of time, existing real-time BDI implementations overlook the temporal implications during the agent’s decision process that may result in delays or unresponsiveness of the system when it gets overloaded. In this paper, we redefine the BDI agent control loop inspired by traditional and well establish algorithms for real-time systems to ensure a proper reaction of agents and their effective application in typical real-time domains. Our model proposes an effective real-time management of goals, plans, and actions with respect to time constraints and resources availability. We propose an implementation of the model for a resource-collection video-game and we validate the approach against a set of significant scenarios.

Legal contracts specify requirements for business transactions. As any other requirements specification, contracts may contain errors and violate properties expected by contracting parties. Symboleo was recently proposed as a formal specification language for legal contracts. This paper presents SymboleoPC, a tool for analyzing Symboleo contracts using model checking. It highlights the architecture, implementation and testing of the tool, as well as a scalability evaluation with respect to the size of contracts and properties to be checked through a series of experiments. The results suggest that SymboleoPC can be usefully applied to the analysis of formal specifications of contracts with real-life sizes and structures.

Smart contracts (SCs) are software systems that monitor and control the execution of legal contracts to ensure compliance with the contracts' terms and conditions. They often exploit Internet-of-Things technologies to support their monitoring functions, and blockchain technology to ensure the integrity of their data. Ethereum and business blockchain platforms, such as Hyperledger Fabric, are popular choices for SC development. However, there is a gap in the knowledge of SCs between developers and legal experts. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo specifications directly encode legal concepts such as parties, obligations, and powers. In this paper, we propose a tool-supported method for translating Symboleo specifications into smart contracts. We have extended the current Symboleo IDE, implemented the ontology and semantics of Symboleo into a reusable library, and developed the Symboleo2SC tool to generate Hyperledger Fabric code exploiting this library. Symboleo2SC was evaluated with three sample contracts. The results shows that legal contract specifications in Symboleo can be fully converted to SCs for monitoring purposes. Moreover, Symboleo2SC helps simplify the SC development process, saves development effort, and helps reduce risks of coding errors.

Planning with global state constraints is an extension of classical planning such that some properties of each state are derived via a set of rules common to all states. This approach is important for the application of planning techniques in manipulating cyber-physical systems, and has been shown to be effective in practice. Urban Traffic Control (UTC) deals with the control and management of traffic in urban regions, and includes the optimisation of traffic signals configuration to minimise traffic congestion and travel delays. In this paper, we briefly introduce how to cast the UTC problem into the formalism of planning with global state constraints, and we perform a preliminary experimental evaluation considering significant scenarios taken from the literature, and a new one based on real-world data. The results show that the approach is feasible, and the quality of generated solutions has been confirmed in simulation using existing symbolic models.

Abstract In this paper, we consider the problem of model checking fair transition systems expressed symbolically in the framework of Satisfiability Modulo Theories. This problem, referred to as Verification Modulo Theories, is tackled by combining two key elements from the legacy of Ed Clarke: SAT-based verification and abstraction refinement. We show how fundamental SAT-based algorithms have been lifted to deal with the extended expressiveness with a tight integration of abstraction within a CEGAR loop. In turn, the case of nonlinear theories is based on a CEGAR loop over the linear case. These two elements have also deeply impacted the development of the NuSMV model checker, born from a joint project between FBK and CMU, and its successor nuXmv, whose core integrates SMT-based techniques for VMT.

Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy. We rely on model-based reasoning, and we consider many important (on-line and off-line) reasoning capabilities such as plan generation, validation, execution and monitoring, runtime diagnosis, and fault detection, identification, and recovery. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, and we have integrated it within an on-board Autonomous Reasoning Engine. Finally, we have evaluated our approach on three case-studies inspired by real-world projects and characterized it in terms of reliability, availability, and performance.

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (à la Satisfiability Modulo Theories (SMT)). We show that the “at next” and “at last” can encode (first-order) MTL0,∞with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in thenuXmvmodel checker enabling the analysis of LTL-EFand MTL0,∞based on SMT-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

nuXmv is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include $$\textsc {MTL}_{0,\infty }$$ formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing nuXmv with other verification tools for timed automata and $$\textsc {MTL}_{0,\infty }$$ , considering different benchmarks from the literature. The results show that nuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for $$\textsc {MTL}_{0,\infty }$$ .

In the context of formal verification, certifying proofs are proofs of the correctness of a model in a deduction system produced automatically as outcome of the verification. They are quite appealing for high-assurance systems because they can be verified independently by proof checkers, which are usually simpler to certify than the proof-generating tools. Model checking is one of the most prominent approaches to formal verification of temporal properties and is based on an algorithmic search of the system state space. Although modern algorithms integrate deductive methods, the generation of proofs is typically restricted to invariant properties only. In this paper, we solve this issue in the context of Linear-time Temporal Logic. By exploiting the k-liveness algorithm, we show how to extend proof generation capabilities for invariant checking to cover full LTL properties, in a simple and efficient manner, with essentially no overhead for the model checker. We implemented the technique on top of an IC3 engine, and show the feasibility of the approach on a variety of benchmarks.

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this article, we tackle the problems of SMT and VMT over the theories of nonlinear arithmetic over the reals (NRA) and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA). We propose a new abstraction-refinement approach for SMT and VMT on NRA or NTA, called Incremental Linearization . The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract space limited to linear arithmetic on the rationals with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the M ath SAT SMT solver and in the nu X mv model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach.

Temporal planning is an active research area of Artificial Intelligence because of its many applications ranging from roboticsto logistics and beyond. Traditionally, authors focused on theautomatic synthesis of plans given a formal representation of thedomain and of the problem. However, the effectiveness of suchtechniques is limited by the complexity of the modeling phase: it ishard to produce a correct model for the planning problem at hand. In this paper, we present a technique to simplify the creation ofcorrect models by leveraging formal-verification tools for automaticvalidation. We start by using the ANML language, a very expressivelanguage for temporal planning problems that has been recentlypresented. We chose ANML because of its usability andreadability. Then, we present a sound-and-complete, formal encodingof the language into Linear Temporal Logic over predicates withinfinite-state variables. Thanks to this reduction, we enable theformal verification of several relevant properties over the planningproblem, providing useful feedback to the modeler.

The Temporal Network with Uncertainty (TNU) modeling framework is used to represent temporal knowledge in presence of qualitative temporal uncertainty. Dynamic Controllability (DC) is the problem of deciding the existence of a strategy for scheduling the controllable time points of the network observing past happenings only. In this paper, we address the DC problem for a very general class of TNU, namely Disjunctive Temporal Network with Uncertainty. We make the following contributions. First, we define strategies in the form of an executable language; second, we propose the first decision procedure to check whether a given strategy is a solution for the DC problem; third we present an efficient algorithm for strategy synthesis based on techniques derived from Timed Games and Satisfiability Modulo Theory. The experimental evaluation shows that the approach is superior to the state-of-the-art.

IC3 is one of the most successful algorithms for hardware model checking. Since its invention in 2010, several variants of the original algorithm have been published, proposing optimizations and/or alternative procedures for many different steps of the algorithm. In this paper, we present a thorough empirical comparison of a large set of optimizations and procedures for the steps of IC3, considering “high-level” variants/extensions to the basic algorithm, as well as “low-level” optimizations/configuration settings. We implemented each of them in the same tool, optimizing the implementations to the best of our knowledge. This enabled for a flexible experimentation in a controlled environment, and to gain new insights about their most important differences and commonalities, as well as about their performance characteristics. We conducted the experiments using as benchmarks the problems used in the last four editions of the hardware model checking competition. The analysis helped us to identify several settings leading to significant improvements with respect to a basic implementation of IC3.

In many practical domains, planning systems are required to reason about durative actions. A common assumption in the literature is that the executor is allowed to decide the duration of each action. However, this assumption may be too restrictive for applications. In this paper, we tackle the problem of temporal planning with uncontrollable action durations. We show how to generate robust plans,that guarantee goal achievement despite the uncontrollability of the actual duration of the actions. We extend the state-space temporalplanning framework, integrating recent techniques for solving temporalproblems under uncertainty. We discuss different ways of lifting the total order plans generated by the heuristic search to partial orderplans, showing (in)completeness results for each of them. We implemented our approach on top of COLIN, a state-of-the-art planner. An experimental evaluation over several benchmark problems shows the practical feasibility of the proposed approach.

The framework of temporal problems with uncertainty (TPU) is useful to express temporal constraints over a set of activities subject to uncertain (and uncontrollable) duration. In this work, we focus on the most general class of TPU, namely disjunctive TPU (DTPU), and consider the case of weak controllability, that allows one to model problems arising in practical scenarios (e.g. on-line scheduling). We first tackle the decision problem, i.e. whether there exists a schedule of the activities that, depending on the uncertainty, satisfies all the constraints. We propose a logical approach, based on the reduction to a problem of Satisfiability Modulo Theories (SMT), in the theory of Linear Real Arithmetic with Quantifiers. This results in the first implemented solver for weak controllability of DTPUs. Then, we tackle the problem of synthesizing control strategies for scheduling the activities. We focus on strategies that are amenable for efficient execution. We prove that linear strategies are not always sufficient, even in the sub-case of simple TPU (STPU), while piecewise-linear strategies, that are multiple conditionally-applied linear strategies, are always sufficient. We present several algorithms for the synthesis of linear and piecewise-linear strategies, in case of STPU and of DTPU. All the algorithms are implemented on top of SMT solvers. We provide experimental evidence of the scalability of the proposed techniques, with dramatic speed-ups in strategy execution compared to on-line reasoning.

A Simple Temporal Network with Uncertainty (STNU) is a structure for representing and reasoning about temporal constraints in domains where some temporal durations are not controlled by the executor. The most important property of an STNU is whether it is dynamically controllable (DC) whether there exists a strategy for executing the controllable time-points that guarantees that all constraints will be satisfied no matter how the uncontrollable durations turn out. This paper provides a novel mapping from STNUs to Timed Game Automata (TGAs) that: (1) explicates the deep theoretical relationships between STNUs and TGAs; and (2) enables the memoryless strategies generated from the TGA to be transformed into equivalent STNU execution strategies that reduce the real-time computational burden for the executor. The paper formally proves that the STNU-to-TGA encoding properly captures the execution semantics of STNUs.

Temporal networks are data structures for representing and reasoning about temporal constraints on activities. Many kinds of temporal networks have been defined in the literature, differing in their expressiveness. The simplest kinds of networks have polynomial algorithms for determining their consistency or controllability, but corresponding algorithms for more expressive networks (e.g., Those that include observation nodes or disjunctive constraints) have so far been unavailable. However, recent work has introduced a new approach to such algorithms based on translating temporal networks into Timed Game Automata (TGAs) and then using off-the-shelf software to synthesize execution strategies -- or determine that none exist. So far, that approach has only been used on Simple Temporal Networks with Uncertainty, for which polynomial algorithms already exist. This paper extends the temporal-network-to-TGA approach to accommodate observation nodes and disjunctive constraints. Insodoing the paper presents, for the first time, sound and complete algorithms for checking the dynamic controllability of these more expressive networks. The translations also highlight the theoretical relationships between various kinds of temporal networks and the TGA model. The new algorithms have immediate applications in the workflow models being developed to automate business processes, including in the health-care domain.

Timelines are a formalism to model planning domains where the temporal aspects are predominant, and have been used in many real-world applications. Despite their practical success, a major limitation is the inability to model temporal uncertainty, i.e. the plan executor cannot decide the duration of some activities.In this paper we make two key contributions. First, we propose a comprehensive, semantically well founded framework that (conservatively) extends with temporal uncertainty the state of the art timeline approach. Second, we focus on the problem of producing time-triggered plans that are robust with respect to temporal uncertainty, under a bounded horizon. In this setting, we present the first complete algorithm, and we show how it can be made practical by leveraging the power of Satisfiability Modulo Theories.

SystemC is an increasingly used language for writing executable specifications of systems-on-chip. The verification of SystemC, however, is a very difficult challenge. Simulation features great scalability, but can miss important defects. On the other hand, formal verification of SystemC is extremely hard because of the presence of threads, and the intricacies of the communication and scheduling mechanisms. In this paper, we explore formal verification for SystemC by means of software model checking techniques, which have demonstrated substantial progress in recent years. We propose an accurate model of SystemC and three complementary encodings of SystemC to finite-state processes, sequential and threaded programming models. We implement the proposed approaches in a tool chain and carry out a thorough experimental evaluation using several benchmarks taken from the literature on SystemC verification, and experimenting with different state-of-the-art software model checkers. The results clearly show the applicability and efficiency of the proposed approaches. In particular, the results show the effectiveness of the threaded and of the finite-model encodings to prove and disprove properties, respectively.

Temporal problems with uncertainty are a well established formalism to model time constraints of a system interacting with an uncertain environment. Several works have addressed the definition and the solving of controllability problems, and three degrees of controllability have been proposed: weak, strong, and dynamic. In this work we focus on weak controllability: we address both the decision and the strategy extraction problems. Extracting a strategy means finding a function from assignments to uncontrollable time points to assignments to controllable time points that fulfills all the temporal constraints. We address the two problems in the satisfiability modulo theory framework. We provide a clean and complete formalization of the problems, and we propose novel techniques to extract strategies. We also provide experimental evidence of the scalability and efficiency of the proposed techniques.

Flaws in requirements may have unacceptable consequences in the development of safety-critical applications. Formal approaches may help with a deep analysis that takes care of the precise semantics of the requirements. However, the proposed solutions often disregard the problem of integrating the formalization with the analysis, and the underlying logical framework lacks either expressive power, or automation. We propose a new, comprehensive approach for the validation of functional requirements of hybrid systems, where discrete components and continuous components are tightly intertwined. The proposed solution allows to tackle problems of conversion from informal to formal, traceability, automation, user acceptance, and scalability. We build on a new language, othello which is expressive enough to represent various domains of interest, yet allowing efficient procedures for checking the satisfiability. Around this, we propose a structured methodology where: informal requirements are fragmented and categorized according to their role; each fragment is formalized based on its category; specialized formal analysis techniques, optimized for requirements analysis, are finally applied. The approach was the basis of an industrial project aiming at the validation of the European Train Control System (ETCS) requirements specification. During the project a realistic subset of the ETCS specification was formalized and analyzed. The approach was positively assessed by domain experts.

Deep space missions are characterized by severely constrained communication links and often require intervention from Ground to overcome the difficulties encountered during the mission. An adequate Ground control could be compromised due to communication delays and required Ground decision-making time, endangering the system, although safing procedures are strictly adhered to. To meet the needs of future missions and increase their scientific return, space systems will require an increased level of autonomy on-board. We propose a comprehensive approach to on-board autonomy relying on model-based reasoning. This approach encompasses in a uniform formal framework many important reasoning capabilities needed to achieve autonomy (such as plan generation, plan validation, plan execution and monitoring, fault detection identification and recovery, run-time diagnosis, and model validation). The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. In this approach we separate out the discrete control parts and the continuous parts of the domain model (e.g., resources such as the power consumed or produced and the data acquired during an execution of a certain action) to facilitate the deliberative actions. The continuous part is associated to the discrete part by means of the resource estimation functions, that are taken into account while validating the generated plan and while monitoring the execution of the current plan. We have developed a prototype of this framework and we have plugged it within an Autonomous Reasoning Engine. This engine has been evaluated on two case studies inspired by real-world ongoing projects: a planetary rover and an orbiting spacecraft. We have performed a characterization of the approach in terms of reliability, availability and performances both on a desktop platform and on a spacecraft simulator.

This paper presents a component-based modelling approach to system-software co-engineering of real-time embedded systems, in particular aerospace systems. Our method is centred around the standardized Architecture Analysis and Design Language (AADL) modelling framework. We formalize a significant subset of AADL, incorporating its recent Error Model Annex for modelling faults and repairs. The major distinguishing aspects of this component-based approach are the possibility to describe nominal hardware and software operations, hybrid (and timing) aspects, as well as probabilistic faults and their propagation and recovery. Moreover, it supports dynamic (i.e. on-the-fly) reconfiguration of components and inter-component connections. The operational semantics gives a precise interpretation of specifications by providing a mapping onto networks of event-data automata. These networks are then subject to different kinds of formal analysis such as model checking, safety and dependability analysis and performance evaluation. Mature tool support realizes these analyses. The activities reported in this paper are carried out in the context of the correctness, modelling, and performance of aerospace systems, project which is funded by the European Space Agency.

We address the problem of computing the exact abstraction of a program with respect to a given set of predicates, a key computation step in Counter-Example Guided Abstraction Refinement. We build on a recently proposed approach that integrates BDD-based quantification techniques with SMT-based constraint solving to compute the abstraction. We extend the previous work in three main directions. First, we propose a much tighter integration of the BDD-based and SMT-based reasoning where the two solvers strongly collaborate to guide the search. Second, we propose a technique to reduce redundancy in the search by blocking already visited models. Third, we present an algorithm exploiting a conjunctively partitioned representation of the formula to quantify. This algorithm provides a general framework where all the presented optimizations integrate in a natural way. Moreover, it allows to overcome the limitations of the original approach that used a monolithic BDD representation of the formula to quantify. We experimentally evaluate the merits of the proposed optimizations, and show how they allow to significantly improve over previous approaches.

The European Train Control System (ETCS) is a control system for the interoperability of the railways across Europe.

The precise computation of abstractions is a bottleneck in many approaches to CEGAR-based verification. In this paper, we propose a novel approach, based on the use of structural information. Rather than computing the abstraction as a single, monolithic quantification, we provide a structure-aware abstraction algorithm, based on two complementary steps. The first, highlevel step exploits the structure of the system, and partitions the abstraction problem into the combination of several smaller abstraction problems. This is represented as a formula with quantifiers. The second, low-level step exploits the structure of the formula, in particular the occurrence of variables within the quantifiers, and applies a set of low-level rewriting rules aiming at further reducing the scope of quantifiers. We experimentally evaluate the approach on a substantial set of benchmarks, and show significant speed ups compared to monolithic abstraction algorithms.

We present the EuRailCheck tool, which supports the formalization and the validation of requirements, based on the use of formal methods. The tool allows the user to analyze the requirements in natural language and to categorize and structure them. It allows to formalize the requirements into a subset of UML enriched with static and temporal constraints for which we defined a formal semantics. Finally, the tool allows to apply model checking techniques specialized for the validation of formal requirements. The tool has been developed and validated within a project funded by the European Railway Agency for the validation of the European Train Control System specification. By now, the tool has been successfully used by about thirty railway experts of different companies.

This paper presents a model-based approach to system-software co-engineering which is focused on aerospace systems but is relevant to a much wider class of dependable systems. We present the main ingredients of the SLIM modeling language and give a precise interpretation of SLIM models by providing a formal semantics using networks of event-data automata. The major distinguishing aspects of this component-based approach are the possibility to describe nominal hardware and software operations, hybrid (and timing) aspects, as well as probabilistic faults and their propagation and recovery. As our approach bears strong resemblance to the standardized AADL (Architecture Analysis and Design Language), a secondary contribution of this paper is a formal semantics of a large fragment of AADL including its Error Model Annex.

This paper reports on a model-based approach to system-software co-engineering which is tailored to critical on-board systems for the aerospace domain but is relevant to a much wider class of dependable systems. Our main contribution is a formal semantics for a greater part of standardised AADL, the Architecture Analysis and Design Language, and its Error Model Annex. It covers nominal and degraded hardware/software operations, hybrid (and timing) aspects as well as probabilistic faults, their propagation and recovery. The accompanying software toolset employs SAT-based and symbolic model checking techniques and probabilistic variants thereof. The precise nature of these techniques together with the formal semantics provide a trustworthy modelling and analysis framework to support, among others, assessment of functional correctness, evaluation of performance measures and automated derivation of dynamic fault trees, FMEA tables and observability requirements.

Flaws in requirements often have a negative impact on the subsequent development phases. In this paper, we propose a novel formalism for the formal representation and validation of requirements. The formalism allows us to represent and reason about object models and their temporal evolution. The key ingredients are class diagrams to represent the objects in the scenarios, fragments of first order logic to deal with the relationships between their attributes and with rich data, and elements of temporal logic operators to deal with the dynamic evolution of the scenario.Formal validation is carried out by means of satisfiability checking, for which we propose a novel procedure based on the reduction to checking the language non-emptiness of a fair transition system.

The IEEE standard Property Specification Language (PSL) is increasingly used in many phases of the hardware design cycle, from specification to verification. PSL combines Linear Temporal Logic (LTL) with Sequential Extended Regular Expressions (SEREs) and, thus, provides a natural formalism to express all$\omega$-regular properties. In this paper, we propose a new method for efficiently converting PSL formulas into symbolically represented Nondeterministic (Generalized) BÜchi Automata (NGBA) that are typically used in many verification and analysis tools. The construction is based on a normal form that separates the LTL and the SERE components, and allows for a modular and specialized encoding. The compilation is enhanced by a set of syntactic transformations that aim at reducing the state space of the resulting NGBA. These rules enable to achieve, at low cost, the simplification that can be achieved with expensive semantic techniques based on minimization. A thorough experimental analysis over large sets of paradigmatic properties (from patterns of properties commonly used in practice) shows that our approach drastically reduces the compilation time and positively affects the overall search time.

The efficient computation of exact abstractions of a concrete program for a given set of predicates is key to the efficiency of Counter-Example Guided Abstraction-Refinement (CEGAR). Recent work propose the use of DPLL-based SMT solvers, modified into enumerators. This technique has been successfully applied in the realm of software, where a control flow graph is available to direct the exploration. However this approach shows some limitations when the number of models grows: in fact, it intrinsically relies on the enumeration of all the implicants, which basically requires the enumerations of all the disjuncts in the DNF of the abstraction. In this paper, we propose a new technique to improve the construction of abstractions. We complement SMT solvers with the use of BDDs, which enables us to avoid the model explosion. Essentially, we exploit the fact that BDDs are a DAG representations of the space that a DPLL-based enumerator treats as a tree. A preliminary experimental evaluation shows the potential of the approach.

Formal languages are increasingly used to describe the functional requirements (specifications) of circuits. These requirements are used as a means to communicate design intent and as basis for verification. In both settings it is of utmost importance that the specifications are of high quality. However, formal requirements are seldom the object of validation, even though they can be hard to understand and interactions between them can be subtle. In this paper we present techniques and guidelines to explore and assure the quality of a formal specification. We define a technique to interactively explore the semantics of a specification by simulating its behavior for user-defined scenarios. Further-more, we define techniques to automatically check specifications against a set of user-provided assertions, which must be satisfied, and a set of possibilities, which must not be conradicted. The proposed techniques support the user in the iterative development and refinement of high-quality specifications.

The IEEE standard property specification language (PSL) allows to express all omega-regular properties mixing linear temporal logic (LTL) with sequential extended regular expressions (SEREs), and is increasingly used in many phases of the hardware design cycle, from specification to verification. Many verification engines are able to manipulate nondeterministic Buchi automata (NBA), that can represent omega-regular properties. Thus, the ability to convert PSL into NBA is an important enabling factor for the reuse of a large wealth of verification tools. Recent works propose a two-step conversion from PSL to NBA: first, the PSL property is encoded into an alternating Buchi automaton (ABA); then, the ABA is converted into an NBA with variants of Miyano-Hayashi's construction. These approaches are problematic in practice: in fact, they are often unable to carry out the conversion in acceptable time, even for PSL specifications of moderate size. In this paper, we propose a modular encoding of PSL into symbolically represented NBA. We convert a PSL property into a normal form that separates the LTL and the SERE components. Each of these components can be processed separately, so that the NBA corresponding to the original PSL property is presented in the form of an implicit product, delaying composition until search time. Our approach has two other advantages: first, we can leverage mature techniques for the LTL components; second, we leverage the particular form of the PSL components that appear in the normal form to improve over the general translation. The transformation is proved correct. A thorough experimental analysis over large sets of paradigmatic properties (from patterns of properties commonly used in practice) shows that our approach drastically reduces the construction time of the symbolic NBA, and positively affects the overall verification time

Formal Tropos is a specification language for early requirements. It is based on concepts from an agent-oriented early requirement model framework (i/sup */) and extends them with a rich temporal specification language. We demonstrated through a small case study how model checking could be used to verify early requirements written in Formal Tropos. We address issues of methodology and scalability for our earlier proposal. In particular, we propose guidelines for producing a Formal Tropos specification from an i/sup */ diagram and for deciding what model checking technique to use when a particular formal property is to be validated. We also evaluate the scope and scalability of our proposal using a tool, the T-Tool, that maps Formal Tropos specifications to a language that can be handled by NUSMV, a state-of-the-art model checker. Our experiments are based on a course management case study.

We tackle the problem of planning in nondeterministic domains, by presenting a new approach to conformant planning. Conformant planning is the problem of finding a sequence of actions that is guaranteed to achieve the goal despite the nondeterminism of the domain. Our approach is based on the representation of the planning domain as a finite state automaton. We use Symbolic Model Checking techniques, in particular Binary Decision Diagrams, to compactly represent and efficiently search the automaton. In this paper we make the following contributions. First, we present a general planning algorithm for conformant planning, which applies to fully nondeterministic domains, with uncertainty in the initial condition and in action effects. The algorithm is based on a breadth-first, backward search, and returns conformant plans of minimal length, if a solution to the planning problem exists, otherwise it terminates concluding that the problem admits no conformant solution. Second, we provide a symbolic representation of the search space based on Binary Decision Diagrams (BDDs), which is the basis for search techniques derived from symbolic model checking. The symbolic representation makes it possible to analyze potentially large sets of states and transitions in a single computation step, thus providing for an efficient implementation. Third, we present CMBP (Conformant Model Based Planner), an efficient implementation of the data structures and algorithm described above, directly based on BDD manipulations, which allows for a compact representation of the search layers and an efficient implementation of the search steps. Finally, we present an experimental comparison of our approach with the state-of-the-art conformant planners CGP, QBFPLAN and GPT. Our analysis includes all the planning problems from the distribution packages of these systems, plus other problems defined to stress a number of specific factors. Our approach appears to be the most effective: CMBP is strictly more expressive than QBFPLAN and CGP and, in all the problems where a comparison is possible, CMBP outperforms its competitors, sometimes by orders of magnitude.