Keynotes & Tutorials

Title: Some applications of formal methods

Abstract: This talk will present some applications of formal methods for aerospace and geoinformatics systems. Firstly, it will be discussed the feasibility, in the context of space systems such as satellites, of probabilistic model checking to the mitigation problem of single event upsets (SEUs) in field-programmable gate arrays (FPGAs). Secondly, it will be presented a method for automated unit test case/data generation based on functional model checking and focusing on C++ source code. The method was applied to two geoinformatics software products. Finally, the topic will be the assessment of the safety of navigation systems for a civil commercial transport category aircraft via probabilistic model checking. Considering these applications, strengths and weaknesses of such formal methods will also be addressed during the talk.

Title: Taming monsters with dragons: a fractal approach to digital twin pipelines

Slides

Abstract: This presentation will discuss how development pipelines evolve over the systems lifecycle to integrate systems and its embedded software, resulting in a digital twin to enable system qualification and auditable artifacts. We will also touch on how the Europa Clipper project leverages such pipelines.

Title: Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community

Slides

Abstract: Safety-critical and security-critical systems are entering our lives at an increasingly rapid pace. These are the systems that help fly our planes, drive our cars, deliver our packages, ensure our electricity, or even automate our homes. Especially when humans cannot perform a task in person, e.g., due to a dangerous working environment, we depend on such systems. Before any safety-critical system launches into the human environment, we need to be sure it is really safe. Model checking is a popular and appealing way to rigorously check for safety: given a system, or an accurate model of the system, and a safety requirement, model checking is a "push button" technique to produce either a proof that the system always operates safely, or a counterexample detailing a system execution that violates the safety requirement. Many aspects of model checking are active research areas, including more efficient ways of reasoning about the system's behavior space, and faster search algorithms for the proofs and counterexamples.

As model checking becomes more integrated into the standard design and verification process for safety-critical systems, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don't have support for expressive specification languages needed for verifying real systems. Our goal is to fill the current gap in model checking research platforms: building a freely-available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the-art back-end algorithms to provide an extensible research and verification tool. We are creating a community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances. To add new modeling languages or algorithms, researchers need only to develop a translator to/from the new intermediate language, and will then be able to integrate each advance with the full state-of-the-art in model checking. This community infrastructure will be ideal for catapulting formal verification efforts in many cutting-edge application areas, including security, networking, and operating system verification. We particularly target outreach to the embedded systems (CPS) community as our new framework will make hardware verification problems from this community more accessible.

Title: Cooperative Verification

Slides

Abstract: Cooperative verification is an approach where several verifiers help each other solving the verification problem by sharing artifacts about the verification task. There are many verification tools available, but the power of combining them is not yet fully leveraged. The problem is that in order to use verifiers 'off-the-shelf', we need clear interfaces to invoke the tools and to pass information. Part of the interfacing problem is to define standard artifacts to be passed between verifiers. We explain a few recent approaches for cooperative combinations and also give a brief overview of CoVeriTeam, a tool for composing verification systems from existing off-the-shelf components.