Uncertainties occur in different forms: data may be noisy, mechanisms may be inherently randomised, the visibility (of e.g. a robot) may not be optimal, and the environment in which a system needs to operate may behave in an unknown manner. The central question that we will address is “Can we guarantee that AI systems are safe and resilient in the presence of such uncertainty?” We advocate using model-based, formal verification and synthesis with a particular focus on automation. We will present techniques to (a) verify uncertainty aspects modeled as randomness and to (b) use formal synthesis to complete partial designs. Several example AI models—Bayesian networks, partially observable Markov decision processes, and probabilistic programs – will illustrate the capabilities of these approaches.
Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.
Compared to semantics with preemptively executing threads, ones with cooperative threads permit easier specification of atomicity in concurrent programs. We introduce a semantics of cooperative programs, and a simulation notion compatible with rely-guarantee proofs. We prove our simulation composes in parallel and sequentially, and that it can establish a standard trace-based notion of refinement.
Runtime verification of temporal properties over timed observations is essential in cyber-physical systems such as autonomous vehicles, smart grids, and medical devices. This talk presents recent advances in predicting property satisfaction or violation in continuous real-time settings. We focus on monitoring properties expressed in Metric Interval Temporal Logic (MITL) or Timed Büchi Automata [2, 4]. Our symbolic online algorithms exploit zone-based techniques from Timed Automata model checking, enabling efficient handling of challenges like time divergence, timing uncertainty, and fluctuating parametric delays–without relying on costly parametric verification. Assumptions about system behavior, expressed as Timed Automata, can further enhance monitoring [1]. We propose an assumption-based runtime verification framework and discuss its extension to probabilistic settings using Stochastic Timed Automata. Implemented in UPPAAL, our algorithms show promising initial results. Finally [3], we also present new findings on monitorability, showing decidability and computable verdict bounds for deterministic Timed Muller Automata, while proving undecidability for nondeterministic Timed Büchi Automata. In addition we introduce and settle decidability of step- and time-bounded monitorability.
We present a summary of a domain analysis description method. Domains are the realm in which [large scale] software is embedded – in order to serve human actions in predominantly man-made “surroundings”. The method, with its principles, procedures, techniques and tools, are outlined. A main principle is that of delineating observable phenomena into describable entities; these into endurants and perdurants, i.e., roughly speaking “statically” and “dynamically” observable entities; entities into endurants and perdurants; endurants into solids and fluids; solids into parts and living species; parts into atomic and compound parts; and compound parts into Cartesians and part sets. Endurants are then “endowed” with unique identities, mereologies, attributes and intentional “pull”. Endurants are then, by transcendental deduction, “morphed” into perdurants: behaviours that communicate, and where unique identities, mereologies and attributes serve as possible updateable behaviour arguments.
