From Simulation to Runtime Verification and Back: Connecting Single-Run Verification Techniques

AbstractRuntime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show that black-box monitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest a gray-box approach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property called distributed data minimization which cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept tool Minion. We describe the tool and apply it to a few case studies to show its feasibility.

Download Full-text

On Dependability Issues in Ambient Intelligence Systems

Pervasive and Ubiquitous Technology Innovations for Ambient Intelligence Environments ◽

10.4018/978-1-4666-2041-4.ch014 ◽

2014 ◽

pp. 146-155

Author(s):

Marcello Cinque ◽

Antonio Coronato ◽

Alessandro Testa

Keyword(s):

Assisted Living ◽

Intelligent Systems ◽

Ambient Intelligence ◽

Ambient Assisted Living ◽

Runtime Verification ◽

Smart Environments ◽

Smart Systems ◽

Computing Paradigm ◽

Ambient Intelligent ◽

Verification Techniques

Ambient Intelligence (AmI) is the emerging computing paradigm used to build next-generation smart environments. It provides services in a flexible, transparent, and anticipative manner, requiring minimal skills for human-computer interaction. Recently, AmI is being adapted to build smart systems to guide human activities in critical domains, such as, healthcare, ambient assisted living, and disaster recovery. However, the practical application to such domains generally calls for stringent dependability requirements, since the failure of even a single component may cause dangerous loss or hazard to people and machineries. Despite these concerns, there is still little understanding on dependability issues in Ambient Intelligent systems and on possible solutions. This paper provides an analysis of the AmI literature dealing with dependability issues and to propose an innovative architectural solution to such issues, based on the use of runtime verification techniques.

Download Full-text

From Simulation to Runtime Verification and Back: Connecting Single-run Verification Techniques

Annual Simulation Symposium (ANSS 2019) ◽

10.22360/springsim.2019.anss.027 ◽

2019 ◽

Keyword(s):

Runtime Verification ◽

Verification Techniques

Download Full-text

Formal Verification of Control System Software

10.23943/princeton/9780691181301.001.0001 ◽

2019 ◽

Author(s):

Pierre-Loïc Garoche

Keyword(s):

Control System ◽

Formal Verification ◽

Formal Analysis ◽

Critical Systems ◽

System Software ◽

Unified Approach ◽

Verification Methods ◽

Autonomous Cars ◽

Computer Scientists ◽

Verification Techniques

The verification of control system software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive. The failure of controller software can cost people their lives. This book provides control engineers and computer scientists with an introduction to the formal techniques for analyzing and verifying this important class of software. Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. The book provides a unified approach that is geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. It presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software. As the autonomy of critical systems continues to increase—as evidenced by autonomous cars, drones, and satellites and landers—the numerical functions in these systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.

Download Full-text