Logo: to the web site of Uppsala University

Satisfiability solving is a common technique for formal verification forming the basis of many proof and model checking systems. Failure to show a proof obligation will produce a counterexample or failure trace with typically many thousands or even millions of boolean variables. Interpreting such a counterexample poses a challenge. Even if the individual variables are all understood, it is difficult to form a "big picture" of the situation causing the failure. We consider the case where verification conditions are expressed using concepts from a formal application domain model in a language based on predicate logic or a similar language. We introduce a method to explain verification failures in application domain terms. A measure of the relative relevance of predicates is used to extract the parts of a formula most likely to contribute meaningfully to the explanation. Dependencies between predicates are used to form a branching sequence of successive explanations. These explanations can help a practitioner find faults in the system being verified. The method is demonstrated on examples and compared to other methods.

This empirical study investigates university teachers’ conceptions of the role of mathematics within science, technology, engineering, and mathematics (STEM) higher education disciplines, employing a phenomenographic approach to capture variation among perspectives of educators in chemistry, computer science, geoscience, and physics. Despite the significant reliance on mathematics across these disciplines, little is known about how educators conceptualise its role. Our study aims to contribute to this research by performing a phenomenographic analysis of semi-structured interviews with 16 teachers at a Swedish university. Through our analysis, we identified five hierarchically inclusive categories that represent increasingly sophisticated conceptions of the role of mathematics: as a computational tool, a language for communication, a key to understanding, an agent for development, and a philosophical foundation. These categories reflect both the instrumental and intrinsic roles that mathematics plays within other STEM disciplines, extending previous empirical findings that predominantly focus on students’ conceptions. We aim to raise awareness among educators, encouraging reflection on how their conceptions influence teaching and fostering a deliberate consideration of mathematics’ role in instruction. By understanding these varied conceptions, STEM educators can enhance instructional strategies and support student engagement with mathematics in a more meaningful way.

We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.

A suitable method supported by a toolset with a high degree of automation is a necessity for the successful employment of formal methods in industrial projects.

The GTO toolset and method have been developed, and successfully applied, to formal methods in safety-critical control applications related to railway signalling since the mid 1990s. The toolset and method support the entire formal methods process from writing and validating formal specifications, through modelling of the implementation to formal verification and analysis of verification results. One goal the toolset and method was to make formal methods more competitive by streamlining the process so that -- at least within an established application area -- individual verification tasks could be done in an "assembly line"-like fashion with minimum overhead.

In line with this goal, the toolset is intended for use with configurable systems, where a generic specification is applicable to a family of systems and adapted to a specific system using configuration data.

The functions carried out by the toolset include static checking and simulation of specifications, checking of configuration data, generation of implementation models from PLC program code or relay schematics, simulation of the implementation model, formal verification by refinement proof, and analysis of failed refinement proofs. Refinement proofs are automatically carried out by a satisfiability (SAT) solver of the user's choice, which is interfaced to the main tool.

We will outline the method and functions of the toolset as well as the formal notation -- a simple temporal predicate logic -- used by the toolset.

A formal theory of an application domain can serve a key role in formal specification and verification of systems operating in that domain. This is particularly relevant when working with families of similar systems intended to control some kind of industrial process or function where the control principles are general while the specifics of the system depend on the particular installation the system is intended to control. In such situations a domain theory can facilitate writing generic specifications or implementations for the entire family of systems which can then be configured for each particular installation. Use of concepts defined in the domain theory can also facilitate communication with domain experts without knowledge in formal methods.

An example of such a family is railway signalling systems which all implement the same general signalling principles of ensuring safe train operation, while the exact function of a particular signalling system depends on the railway track layout under its control.

We will give concrete examples from industrial practise in the railway domain, showing how domain theories can help in the formal verification process. The examples include writing and validating formal specifications, formally verifying implementations and analysing and communicating the results of failed verifications.