Formal Specification and Analysis of Autonomous Systems under Partial Compliance

TL;DR

This paper introduces a formal method for specifying and analyzing autonomous systems' partial compliance with requirements under uncertain environments, using probabilistic model checking to evaluate system robustness and resilience.

Contribution

It proposes a novel approach to define weakened specifications as a lattice and explores system behaviors under these specifications to assess safety and correctness.

Findings

Probabilistic model checking effectively evaluates requirement satisfaction.

The approach identifies optimal specifications for system resilience.

Application to a domestic robotic assistant demonstrates practical utility.

Abstract

The widespread adoption of autonomous systems depends on providing guarantees of safety and functional correctness, at both design time and runtime. Information about the extent to which functional requirements can be met in combination with non-functional requirements (NFRs) -- i.e. requirements that can be partially complied with -- , under dynamic and uncertain environments, provides opportunities to enhance the safety and functional correctness of systems at design time. We present a technique to formally define system attributes that can change or be changed to deal with dynamic and uncertain environments (denominated weakened specifications) as a partially ordered lattice, and to automatically explore the system under different specifications, using probabilistic model checking, to find the likelihood of satisfying a requirement. The resulting probabilities form boundaries of "optimal specifications", analogous to Pareto frontiers in multi-objective optimization, informing the designer about the system's capabilities, such as resilience or robustness, when changing its attributes to deal with dynamic and uncertain environments. We illustrate the proposed technique through a domestic robotic assistant example.