Verification-Enhanced Learning for Safe Autonomous Robots

Robots are becoming part of our daily lives in many forms, including vacuum cleaners, lawnmowers, domestic servants, walking and standing supports for the elderly and the disabled. For such robots to be effective, they must be capable of “autonomy”, i.e., the ability to learn and take decisions based on unforeseen circumstances. Autonomy might however conflict with safety which must be guaranteed at all times, but without hampering robot’s operations or making it less effective. The goal of this research is to study how computer-assisted methods can support learning and deployment of robot’s control policies to ensure that they are both effective and safe.

Computer Automated Design of Elevators

Elevators are a widespread automation system, with stringent safety and operational constraints, yet mostly operated by non-technical personnel. Italy is the second market in the world after China in terms of installations with about nine hundred thousands elevators operating. Design of new installations as well as maintenance and adaptation of currently operating ones must cope with several normative guidelines and, at the same time, be time- and cost-effective given the relatively low profit margins. The goal of this research is to develop computer-assisted methods that can support both designers and installers in building and maintaining elevators, enabling them to obtain draft projects and fine tune them starting from basic measurements and essential design choices.

Decision Procedures for Boolean Logics

Boolean logic, together with quantified, modal/temporal and modulo-theory extensions, is a fundamental tool in the modeling and verification of hardware and software systems. However, even when decision problems in such logics admit algorithmic solutions, to the best of the current knowledge they are not computationally tractable, making straightforward application to large-scale problems a challenge. In spite of such theoretical limits, decision procedures for Boolean logics have been shown capable of handling relevant problems whose size far exceeds worst-case complexity results. The ongoing research in heuristics, optimization and pre-processing techniques has a fundamental role in making decision procedures for Boolean logics applicable in practice. Our research in this direction is aimed to improve on the state of the art and enable existing solvers to attack relevant problems in automated verification and reasoning of complex systems.

Verification of High-Level Software Requirements

During the initial phases of a software design, natural language is routinely adopted for succinct communication of high-level requirements between the various stakeholders, e.g., customers, designers, implementers, involved in the design of software systems. However, natural language descriptions can be informal, incomplete, imprecise and ambiguous, and cannot be processed easily by design and analysis tools. Formal languages, on the other hand, formulate design requirements in a precise and unambiguous mathematical notation, but are more difficult to master and use. This line of research aims to provide software engineers with tools that can analyze high level requirements written in natural language and establish whether they fulfill specific style guidelines, e.g., the guideline DO-178B (Software Considerations in Airborne Systems and Equipment Certification). Furthermore, conversion to controlled natural languages and consistency checking by means of equivalent formulations in temporal logics is sought, with the goal of providing improved confidence in the absence of inconsistencies.

Contract-Based Simulation and Verification of Cyber-Physical Systems

A cyber-physical system is an integration of computation with physical processes. Embedded computers and networks monitor and control the physical processes, usually with feedback loops where physical processes affect computations and vice versa. Complexity, robustness, safety and reliability are key issues in the design of cyber-physical systems. Contract-based design helps to address the design complexity using both a compositional approach and contracts to specify components behavior. Simulation is a widespread technique, but it cannot guarantee the absence of bugs, while formal verification techniques can solve the problem of model correctness. Existing tools address those issues separately, while this research aims to a comprehensive approach that would definitely improve system design, reduce costs and development times.