Search

This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study. To this end, it advocates improved teaching of formal methods;systematic highlighting of formal methods within existing, ‘classical’ computer science courses; andthe inclusion of a compulsory formal methods course in computer science and software engineering curricula. These recommendations are based on the observations that formal methods are an essential and cost-effective means to increase software quality; howevercomputer science and software engineering programmes typically fail to provide adequate training in formal methods; and thusthere is a lack of computer science graduates who are qualified to apply formal methods in industry. This white paper is the result of a collective effort by authors and participants of the 1st International Workshop on Formal Methods – Fun for Everybody which was held in Bergen, Norway, 2–3 December 2019. As such, it represents insights based on learning and teaching computer science and software engineering (with or without formal methods) at various universities across Europe.

There is a strong consensus that combining the versatility of machine learning with the assurances given by formal verification is highly desirable. It is much less clear what verified machine learning should mean exactly. We consider this question from the (unexpected?) perspective of computable analysis. This allows us to define the computational tasks underlying verified ML in a model-agnostic way, and show that they are in principle computable.

This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study. To this end, it advocates (i) improved teaching of formal methods; (ii) systematic highlighting of formal methods within existing, `classical' computer science courses; and (iii) the inclusion of a compulsory formal methods course in computer science and software engineering curricula. These recommendations are based on the observations that (a) formal methods are an essential and cost-effective means to increase software quality; however (b) computer science and software engineering programmes typically fail to provide adequate training in formal methods; and thus (c) there is a lack of computer science graduates who are qualified to apply formal methods in industry. This white paper is the result of a collective effort by authors and participants of the 1st International Workshop on "Formal Methods, Fun for Everybody" which was held in Bergen, Norway, 2-3 December 2019. As such, it represents insights based on learning and teaching computer science and software engineering (with or without formal methods) at various universities across Europe.

The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theory.

LIPIcs, Volume 139, CALCO'19, Complete Volume, LIPIcs, Vol. 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), pages 0-0

In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion appears when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the Kandroid tool, which provides an encoding of the Android/Smali code semantics within the K framework. Kandroid allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems., Comment: 2 pages, 2 figures, FTFJP'17

Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we provide a concise definition of collusion and report on a number of automated detection approaches, developed in co-operation with Intel Security.

The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies. The DTU/Bremen research has been funded by the RobustRailS project granted by Innovation Fund Denmark. The Surrey/Swansea research has been funded by the SafeCap and the DITTO research projects granted by EPSRC and RSSB. The authors would like to thank Linh Hong Vu for providing the benchmark of scheme plans and the drawings of the track plans.

We present an institution for UML state machines without hierarchical states. The interaction with UML class diagrams is handled via institutions for guards and actions, which provide dynamic components of states (such as valuations of attributes) but abstract away from details of class diagrams. We also study a notion of interleaving product, which captures the interaction of several state machines. The interleaving product construction is the basis for a semantics of composite structure diagrams, which can be used to specify the interaction of state machines. This work is part of a larger effort to build a framework for formal software development with UML, based on a heterogeneous approach using institutions., Comment: 24 pages. arXiv admin note: substantial text overlap with arXiv:1403.7747

We present a framework for formal software development with UML. In contrast to previous approaches that equip UML with a formal semantics, we follow an institution based heterogeneous approach. This can express suitable formal semantics of the different UML diagram types directly, without the need to map everything to one specific formalism (let it be first-order logic or graph grammars). We show how different aspects of the formal development process can be coherently formalised, ranging from requirements over design and Hoare-style conditions on code to the implementation itself. The framework can be used to verify consistency of different UML diagrams both horizontally (e.g., consistency among various requirements) as well as vertically (e.g., correctness of design or implementation w.r.t. the requirements).

Electronic Communications of the EASST, Volume 62: Specification, Transformation, Navigation - Special Issue Dedicated to Bernd Krieg-Brückner

Electronic Communications of the EASST, Volume 62: Specification, Transformation, Navigation - Special Issue Dedicated to Bernd Krieg-Brückner

CSP-CASL is but one of the many languages for which Bernd Krieg-Brueckner (BKB) had a great deal of influence throughout its development process: from the initial idea of working towards an integration of the process algebra CSP with the algebraic specification language CASL, to the design of the concrete syntax, and also to tool support for CSP-CASL, where the theorem prover Isabelle should provide the common platform. In all this, BKB provided inspiration and guidance, funding, and also a helping hand when needed. This paper provides a survey on the technology developed so far for CSP-CASL, covering results of a theoretical nature, an industrial case study, theorem proving support as well as a testing approach. In honour of BKB’s 60th birthday, this survey documents what has become out of one of BKB’s visions., Electronic Communications of the EASST, Volume 62: Specification, Transformation, Navigation - Special Issue Dedicated to Bernd Krieg-Brückner

Electronic Communications of the EASST, Volume 35: Automated Verification of Critical Systems 2010

In this paper, we demonstrate the successful application of various SAT-based model checking techniques to verify train control systems. Starting with a propositional model for a control system, we show how execution of the system can be modelled via a finite automaton. We give algorithms to perform SAT-based model checking over such an automaton. In order to tackle state-space explosion we propose slicing. Finally we comment on results obtained by applying these methods to verify two real-world railway interlocking systems., Electronic Communications of the EASST, Volume 35: Automated Verification of Critical Systems 2010

Electronic Communications of the EASST, Volume 23: Automated Verification of Critical Systems 2009

Electronic Communications of the EASST, Volume 23: Automated Verification of Critical Systems 2009

Lossy channel systems (LCSs for short) are models for communicating systems where the subprocesses are linked via unbounded FIFO channels which might lose messages. Link protocols, such as the Alternating Bit Protocol and HDLC can be modelled with these systems. The decidability of several verification problems of LCSs has been investigated by Abdulla & Jonsson [AJ93,AJ94], e.g. they have shown that the reachability problem for LCSs is decidable while LT L model checking is not. In this paper, we consider probabilistic LCSs (which are LCSs where the transitions are augmented with appropriate probabilities) as introduced by [IN97] and show that the question of whether or not a linear time property holds with probability 1 is deddable. More precisely, we show how LT L\x model checking for (certain types of) probabilistic LCSs can be reduced to a reachability problem in a (non-probabilistic) LCS where the latter can be solved with the methods of [AJ93].

Bisimulation wurde von Milner (1980) und Park (1981) auf Transitionssystemen eingefuehrt, um Prozesse zu identifizieren, die aus Sicht eines externen Beobachters nicht zu unterscheiden sind. Ausgehend von dieser Idee werden neue Bisimulationsbegriffe auch auf anderen Modellen parallelen Rechnens betrachtet, deren Definition von der Syntax her der urspruenglichen Definition von Bisimulation zumeist aehnlich sieht. Daraus erwaechst die Fragestellung: Was haben diese neuen Bisimulationen mit dem urspruenglichen Begriff zu tun, gibt es mehr als einen nur syntaktischen Zusammenhang zwischen ihnen, laesst sich ein gemeinsamer Ueberbegriff, eine abstrakte Charakterisierung finden? In der Literatur finden sich verschiedene Ansaetze fuer eine abstrakte Charakterisierung von Bisimulation: Degano, De Nicola und Montanari (1993) verwenden spezielle Baeume, Malacaria (1995) arbeitet mit Methoden der Algebra, Aczel und Mendler (1989) einerseits und Joyal, Nielsen und Winskel (1994) andereseits nutzen Begriffe der Kategorientheorie. Wir vergleichen in dieser Arbeit die beiden letztgenannten Ansaetze. Zum einen suchen wir nach direkten Zusammenhaengen zwischen den abstrakten Charakterisierungen. Zum anderen fragen wir uns, ob sich konkrete Bisimulationen auf unterschiedlichen Modellen parallelen Rechnens mittels der abstrakten Charakterisierungen darstellen lassen. Beide Vergleiche lassen den Schluss zu, dass die Charakterisierung von Aczel von den untersuchten Konzepten das umfassendste ist. Von daher beantworten wir die Frage, was eine Bisimulation ist, mit dem Begriff der AM-Bisimulation: Eine Bisimulation zwischen zwei Objekten ist ein Transitionssystem, welches das beobachtbare "Verhalten" wiedergibt, das beiden Objekten gemeinsam ist.

The realm of approaches to operational descriptions and equivalences for concurrent systems in the literature leads to aseries of different attempts to give a uniform characterization of what should be considered as abisimulation, mostly in an algebraic and/or categorical framework. Meanwhile the realm of such approaches calls itselffor comparison and/or unification. We investigate how different abstract characterizations of bisimulations are related and how suitable they are to encompass the various concrete notions of bisimulation.

[AM89] and [JNW94] present abstract concepts of bisimulation in terms of category theory. This paper deals with the question how these approaches are related. Futheron it shows how different types of bisimulations on prime event structures can be modelled in terms of the abstract concepts.

Aczel89 and Joyal94 give distinct characterizations of bisimulation on labelled transition systems in terms of category theory. This paper discusses the differences between their formalisms and shows how to translate these approaches into one another.

This paper adds the technique of chain completion to the setting of [MCB94]. We develop the theory of chain completion Ch(D) of a domain D and show how this completion relates to metric and ideal completion. Especially we study consistency results for denotational semantics on D, Ch(D) and Idl(D).

We discuss what kind of completeness guarantees can be provided by semi-algorithms for the synthesis of the set of parameters under which a parametric timed automata meets some liveness property.

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop's basic process algebra (BPA) with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based. © 2006 Elsevier B.V. All rights reserved.

In this article the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This article explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches.