Abstract Reactive synthesis is the process of automatically generating a correct system from a given temporal specification. In this paper, we address the problem of reactive synthesis for LTL modulo theories ( $$\textrm{LTL}^{\mathcal {T}}$$ LTL T ), which extends LTL with literals from a first-order theory and allows relating the values of data across time . This logic allows describing complex dynamics both for the system and for the environment—such as a numeric variable increasing monotonically over time. The logic also allows defining relations (and not only assignment) between variables, enabling permissive shielding. We propose a sound algorithm called Counter-Example Guided Reactive Synthesis modulo theories (CEGRES), whose core is the novel concept of reactive tautology , which are valid temporal formulas that preserve the semantics of the specification but make the algorithm conclusive. Although realizability for full $$\textrm{LTL}^{\mathcal {T}} $$ LTL T is undecidable in general, we prove that CEGRES is terminating for some important theories and for arbitrary theories when specifications do not fetch data across time. We include an empirical evaluation that shows that CEGRES can solve many reactive synthesis problems of practical interest.

Temporal task planning guarantees a robot will succeed in its task as long as certain explicit and implicit assumptions about the robot’s operating environment, sensors, and capabilities hold. A robot executing a plan can silently fail to fulfill the task if the assumptions are violated at runtime. Monitoring assumption violations at runtime can flag silent failures and also provide mitigation and remediation opportunities. However, this requires means for describing assumptions combining temporal and quantitative data, automatic construction of correct monitors and ensuring a correct interplay between the planning execution and monitors. In this paper we propose combining temporal planning with stream runtime verification, which offers a high-level language to describe monitors together with guarantees on execution time and memory usage. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.

Abstract We present , an extensible Stream Runtime Verification (SRV) tool, that borrows from the functional language Haskell (1) rich types for data in events and verdicts; and (2) functional features for parametrization, libraries, high-order specification transformations, etc. SRV is a formal dynamic analysis technique that generalizes Runtime Verification (RV) algorithms from temporal logics like LTL to stream monitoring, allowing the computation of verdicts richer than Booleans (quantitative values and beyond). The keystone of SRV is the clean separation between temporal dependencies and data computations. However, in spite of this theoretical separation previous engines include hardwired implementations of just a few datatypes, requiring complex changes in the tool chain to incorporate new data types. Additionally, when previous tools implement features like parametrization these are implemented in an ad-hoc way. In contrast, is implemented as a Haskell embedded DSL, borrowing datatypes and functional aspects from Haskell, resulting in an extensible engine (The tool is available open-source at http://github.com/imdea-software/hlola ). We illustrate through several examples, including a UAV monitoring infrastructure with predictive characteristics that has been validated in online runtime verification in real mission planning.

Modern cloud applications are based on microservice architectures. The deployment of these microservice based applications often requires that every constituent service starts after all its dependencies are configured and running properly. It is also common that these dependencies generate dynamic data that needs to be supplied to other services too at starting time. More complex scenarios require additionally interchanging data in other phases of the microservices lifecycle. One alternative to solve these dependencies is to describe the deployment of microservice applications manually—using scripts—which allows IT operators to precisely define when a service is ready to start serving other components. However, synchronization by scripting is tedious, error prone and hard to maintain. Other solutions offer specific languages to describe service dependencies, along with tool support that interpret scripts in these languages to take care of starting services in the proper order. These tools are either very rich but complex to use, or fail in providing sophisticated ways to describe what it means for a service to be ready. Moreover, the communication layer between services, if supplied, is based on intermediate entities and non-trivial network protocols. This paper proposes pipekit as a solution, by offering a container orchestration language which focuses on simplicity (pipekit is similar to Docker Compose) and is equipped with directives to define when a service is ready. The pipekit tool provides a communication layer for moving data between services, implemented using shared storage. This shared storage provides a very simple interface to move artifacts between services, and greatly simplifies the synchronization logic of pipekit by using semaphores at the file system level.

This article reports on our experiences in applying formal methods to verify the security mechanisms of Android. We have developed a comprehensive formal specification of Android's permission model, which has been used to state and prove properties that establish expected behavior of the procedures that enforce the defined access control policy. We are also interested in providing guarantees concerning actual implementations of the mechanisms. Therefore we are following a verification approach that combines the use of idealized models on which fundamental properties are formally verified with testing of actual implementations using lightweight model-based techniques. We describe the formalized model, present security properties that have been verified using the Coq proof assistant and discuss a testing technique that relies on the use of certified algorithms.