Working Group 1: Core runtime verification
This group aims at clarifying the dimensions of runtime verification, its theory, algorithms and methods. These are the activities in which most of the work on RV has focused in the early stages of the discipline, with scattered results based on methods from other areas, notably formal methods and programming languages, and guided by application goals.
Many outcomes from the other working groups will pose new sets of problems and challenges for the core RV community. Specific activities of Working Group 1 will include research actions centered around establishing a common framework for runtime verification, and challenges for new research and technology based on the other working groups. These activities include:
- To establish a taxonomy of runtime verification aspects that “paves the road” to allow a classification and comparison of theoretical results, problems and techniques.
- To identify the challenges and opportunities of instrumentation, where the system under scrutiny is modified or harnessed to allow the monitoring process.
- To study the interplay between runtime verification and static analysis, between runtime verification and model checking, and between runtime verification and testing. All these activities are proposed to increase or assess system’s reliability, but their interplay can potentially increase their applicability. For example, by static analysis one can specialize a system for a monitoring task and a monitor for a specific system, rendering a monitoring task feasible.
- To study applications of runtime verification beyond system observation. This includes reflection to act upon the system, typically to control and prevent errors, or to replay allowing an error to be reproduced or even fixed.
- To pose the challenges in monitoring quantitative and statistical data, beyond property violation.
The concrete output of this Working Group will be collaborative research papers, and a document describing a set of challenges and roadmap for each of the directions described above.
The final document describing the results of the working group is available as WG1-Report.
Working Group 2 aims to clear the landscape of formalisms and tools proposed and built for runtime verification, to design common input formats and to establish a large class of benchmarks and challenges. Among the activities of this working group are the following:
- Enriching of the taxonomy of runtime verification concerns identified in Working Group 1 to classify tools and problems.
- The design of common representation formats for inputs to monitoring tools. The common language will not be a one-size-fits-all approach, as, for example, the definition of event and its data contents, and the dependence between a trace and thesystem that generates the trace varies widely. Instead, the outcome will be more a small family of suitable languages, following the taxonomy developed by Working Group 1
- The implementation of the interfaces in the common format for different programming languages and formalisms to enable that different RV tools can be attached to a variety of different programs and systems.
- The creation and maintenance of a collection of examples in the form of benchmarks, classified according to the taxonomy and expressed in the languages in the common format.
- The coordination of periodical activities for comparing tools against some of the benchmarks. This can take the form of a tool competition.
The concrete outputs of this Working Group will be a common computation infrastructure, including a description of the formats and implementations for programming languages of interest, and a collection of benchmarks.
The final document describing the results of the working group is available as WG2-Report.
This group will study novel and challenging computational domains for runtime verification and monitoring that result from the study of other application areas than programming languages. The objectives of this Working Group will be to identify the challenges for monitoring in the following application domains:
- Distributed systems, where the timing of observations may vary widely in a non-synchronized manner.
- Embedded systems, where the resources of the monitor are constrained.
- Hardware, where the timing must be precise and the monitor must operate non disruptively.
- Unreliable domains and approximated domains, where either the system is not reliable, or aggregation or sampling is necessary due to large amounts of data.
These areas involve expertise from more than one domain and have a much higher chance of success if attacked cooperatively. The concrete outputs of this Working Group will be twofold. First, a series of documents will be worked out giving a roadmap for the application of runtime verification techniques to the areas listed above, identifying connections with established work in the respective sub-areas of computer science, and challenges and opportunities. Second, a concrete case study will performed, in which a runtime verification solution for multicore systems will be developed using dedicated monitoring hardware based on FPGAs to show the feasibility and general applicability of runtime verification techniques.
Results of this working group are given in form of two scientific contributions. First, a overview article listing 47 challenges ranging over 7 domain. This article is accepted by Springer’s journal Formal Methods in System Design (FMSD). A preprint is available here.
This group studies the potential applications of RV to important application areas beyond software and hardware reliability, including medical devices and legal contracts. This task requires the direct interaction with experts from the respective communities. The Working Group will organize workshops with invited experts from application domains. For example, for the safe interoperability of medical devices, it is important to enrich the interface COST specifications with temporal properties about the intended interaction of two devices and to synthesize monitoring code for runtime. If monitoring identifies unwanted behavior, the systems might go into some fail-safe mode. Another interesting application area that will be explored is how to monitor legal e-contracts (e.g., computer-mediated transactions). Some efforts have recently been done to formalize legal contracts using formal languages, where skeletons of runtime monitors could be extracted from the formal semantics. The time is now right to apply these techniques successfully to real case studies, which is planned for this working group. Other applications include robotic and hybrid systems, monitoring for business models and systems security. Concrete output of this Working Group will consist on documents describing challenges and potential applications of runtime verification to these application areas. Moreover, a concrete case study in the medical domain will be performed identifying the safety enhancements of medical devices by using runtime verification techniques. More…