| 1. |
- Åman Pohjola, Johannes
(author)
-
Culling Concurrency Theory : Reusable and trustworthy meta-theory, proof techniques and separation results
- 2016
-
Doctoral thesis (other academic/artistic)abstract
- As concurrent systems become ever more complex and ever more ubiquitous, the need to understand and verify them grows ever larger. For this we need formal modelling languages that are well understood, with rigorously verified foundations and proof techniques, applicable to a wide variety of concurrent systems.Defining modelling languages is easy; there is a stupefying variety of them in the literature. Verifying their foundations and proof techniques, and developing an understanding of their interrelationship with other modelling languages, is difficult, tedious and error-prone. The contributions of this thesis support these tasks in reusable and trustworthy ways, by results that apply to a wide variety of modelling languages, verified to the highest standards of mathematical rigour in an interactive theorem prover.To this end, we extend psi-calculi - a family of process calculi with reusable foundations for formal verification - with several new language features. We prove that the bisimulation meta-theory of psi-calculi carries over to these extended settings. This widens the scope of psi-calculi to important application areas, such as cryptography and wireless communication. We develop bisimulation up-to techniques - powerful proof techniques for showing that two processes exhibit the same observable behaviour - that apply to all psi-calculi. By showing how psi-calculi can encode dynamic priorities under very strong quality criteria, we demonstrate that the expressive power is greater than previously thought. Finally, we develop a simple and widely applicable technique for showing that a process calculus adds expressiveness over another, based on little more than whether parallel components may act independently or not. Many separation results, both novel ones and strengthenings of known results from the literature, emerge as special cases of this technique.
|
|
| 2. |
- Bengtson, Jesper, 1977-
(author)
-
Formalising process calculi
- 2010
-
Doctoral thesis (other academic/artistic)abstract
- As the complexity of programs increase, so does the complexity of the models required to reason about them. Process calculi were introduced in the early 1980s and have since then been used to model communication protocols of varying size and scope. Whereas modeling sophisticated protocols in simple process algebras like CCS or the pi-calculus is doable, expressing the models required is often gruesome and error prone. To combat this, more advanced process calculi were introduced, which significantly reduce the complexity of the models. However, this simplicity comes at a price -- the theories of the calculi themselves instead become gruesome and error prone, establishing their mathematical and logical properties has turned out to be difficult. Many of the proposed calculi have later turned out to be inconsistent.The contribution of this thesis is twofold. First we provide methodologies to formalise the meta-theory of process calculi in an interactive theorem prover. These are used to formalise significant parts of the meta-theory of CCS and the pi-calculus in the theorem prover Isabelle, using Nominal Logic to allow for a smooth treatment of the binders. Second we introduce and formalise psi-calculi, a framework for process calculi incorporating several existing ones, including those we already formalised, and which is significantly simpler and substantially more expressive. Our methods scale well as complexity of the calculi increases.The formalised results for all calculi include congruence results for both strong and weak bisimilarities, in the case of the pi-calculus for both the early and the late operational semantics. For the finite pi-calculus, we also formalise the proof that the axiomatisation of strong late bisimilarity is sound and complete. We believe psi-calculi to be the state of the art of process calculi, and our formalisation to be the most extensive formalisation of process calculi ever done inside a theorem prover.
|
|
| 3. |
- Berg, Therese
(author)
-
Regular inference for reactive systems
- 2006
-
Licentiate thesis (other academic/artistic)abstract
- Models of reactive systems play a central role in many techniques for verification and analysis of reactive systems. Both a specification of the system and the abstract behavior of the system can be expressed in a formal model. Compliance with the functional parts in the specification can be controlled in different ways. Model checking techniques can be applied to a model of the system or directly to source code. In testing, model-based techniques can generate test suites from specification. A bottleneck in model-based techniques is however to construct a model of the system. This work concerns a technique that automatically constructs a model of a system without access to specification, code or internal structure. We assume that responses of the system to sequences of input can be observed. In this setting, so called regular inference techniques build a model of the system based on system responses to selected input sequences.There are three main contributions in this thesis. The first is a survey on the most well-known techniques for regular inference. The second is an analysis of Angluin's algorithm for regular inference on synthesized examples. On a particular type of examples, with prefix-closed languages, typically used to model reactive systems, the required number of input sequences grow approximately quadratically in the number of transitions of the system. However, using an optimization for systems with prefix-closed languages we were able to reduce the number of required input sequences with about 20%. The third contribution is a developed regular inference technique for systems with parameters. This technique aims to better handle entities of communications protocols where messages normally have many parameters of which few determine the subsequent behavior of the system. Experiments with our implementation of the technique confirm a reduction of the required number of input sequences, in comparison with Angluin's algorithm.
|
|
| 4. |
- Johansson, Magnus, 1976-
(author)
-
Psi-calculi: a framework for mobile process calculi : Cook your own correct process calculus - just add data and logic
- 2010
-
Doctoral thesis (other academic/artistic)abstract
- A psi-calculus is an extension of the pi-calculus with nominal data types for data structures, logical assertions, and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Expressiveness and therefore modelling convenience significantly exceed those of other formalisms: psi-calculi can capture the same phenomena as other extensions of the pi-calculus, and can be more general, e.g. by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions.Ample comparisons to related calculi are provided and a few significant applications are discussed. The labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. Minimal requirements on the nominal data and logic are established in order to prove general algebraic properties of psi-calculi. The purity of the semantics is on par with the pi-calculus.The theory of weak bisimulation is established, where the tau actions are unobservable. The notion of barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of weak barbs in all static contexts. It is proved that weak barbed equivalence coincides with weak bisimulation equivalence.A symbolic transition system and bisimulation equivalence is presented, and shown fully abstract with respect to bisimulation congruence in the non-symbolic semantics. The symbolic semantics is necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means processes are bisimilar in the symbolic setting if they are bisimilar in the original semantics.Psi-calculi remove the necessity of proving general properties every time a new mobile process calculus is defined. By properly instantiating the framework the properties are guaranteed to hold, thus removing the need to do tedious and error-prone proofs.
|
|
| 5. |
- Wibling, Oskar, 1973-
(author)
-
Creating Correct Network Protocols
- 2008
-
Doctoral thesis (other academic/artistic)abstract
- Network protocol construction is a complex and error prone task. The challenges originate both from the inherent complexity of developing correct program code and from the distributed nature of networked systems. Protocol errors can have devastating consequences. Even so, methods for ensuring protocol correctness are currently only used to a limited extent. A central reason for this is that they are often complex and expensive to employ. In this thesis, we develop methods to perform network protocol testing and verification, with the goal to make the techniques more accessible and readily adoptable. We examine how to formulate correctness requirements for ad hoc routing protocols used to set up forwarding paths in wireless networks. Model checking is a way to verify such requirements automatically. We investigate scalability of finite-state model checking, in terms of network size and topological complexity, and devise a manual abstraction technique to improve scalability. A methodology combining simulations, emulations, and real world experiments is developed for analyzing the performance of wireless protocol implementations. The technique is applied in a comparison of the ad hoc routing protocols AODV, DSR, and OLSR. Discrepancies between simulations and real world behavior are identified; these are due to absence of realistic radio propagation and mobility models in simulation. The issues are mainly related to how the protocols sense their network surroundings and we identify improvements to these capabilities. Finally, we develop a methodology and a tool for automatic verification of safety properties of infinite-state network protocols, modeled as graph transformation systems extended with negative application conditions. The verification uses symbolic backward reachability analysis. By introducing abstractions in the form of summary nodes, the method is extended to protocols with recursive data structures. Our tool automatically verifies correct routing of the DYMO ad hoc routing protocol and several nontrivial heap manipulating programs.
|
|
| 6. |
- Gengelbach, Arve
(author)
-
Conservative Definitions for Higher-order Logic with Ad-hoc Overloading
- 2021
-
Doctoral thesis (other academic/artistic)abstract
- With an ever growing dependency on computer systems, the need to guarantee their correct behaviour increases. Mathematically rigorous techniques like formal verification offer a way to derive a system's mathematical properties for example with the help of a theorem prover. A theorem prover is a type of software that assists a user in deriving theorems expressed in a formal language. With a theorem prover one should never be able to prove something that is contradictory, as otherwise the proof effort is worthless. This property is called consistency and is essential for formal developments.Theorem provers enjoy high confidence, since they often rely on a trusted logical kernel that is enriched with new symbols in a controlled way. Instead of asserting the existence of mathematical objects with their desired properties, new symbols are introduced through definitions. These definitions are checked by this kernel, and expected to act as abbreviations. Any theorem that is expressible without a definition should not need that definition in its proof. A definition satisfying this property is called conservative. Conservative definitions are especially important as they preserve consistency, so that a proof of a contradiction is not possible after adding these definitions.Isabelle/HOL is a prominent theorem prover with the unique feature of permitting different definitions of one constant at non-overlapping types. In addition to these so-called overloading definitions, a symbol may be used before it is defined. These features mean that consistency or conservativity arguments for simpler logics do not immediately apply to Isabelle/HOL. In the past, design flaws in the definitional mechanism made theories in the Isabelle/HOL theorem prover inconsistent, e.g. it was possible to derive a contradiction from cyclic definitions.With this thesis we show that (overloading) definitions in higher-order logic (HOL) are conservative, hence not source of inconsistency. We define and prove a notion of conservativity that applies to theories of overloading definitions in higher-order logic and formalise aspects of our results in a theorem prover. As a practical implication, when searching for a proof of a formula, our syntactic conservativity criterion allows to exclude irrelevant symbols. In particular, our results confirm that Isabelle/HOL theories are consistent, thus users cannot introduce contradictions through definitions. As a specialisation of our work, our notion of conservativity holds for variants of HOL without overloading. Overall, our work contributes to the understanding of higher-order logic with overloading definitions.
|
|
| 7. |
- Raabjerg, Palle
(author)
-
Extending psi-calculi and their formal proofs
- 2012
-
Licentiate thesis (other academic/artistic)abstract
- Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. This thesis presents broadcast psi-calculi and higher-order psi-calculi, two extensions of the psi-calculi framework, allowing respectively one-to-many communications and the use of higher-order process descriptions through conditions in the parameterised logic. Both extensions preserve the purity of the psi-calculi semantics; the standard congruence and structural properties of bisimilarity are proved formally in Isabelle. The work going into the extensions show that depending on the specific extension, working out the formal proofs can be a work-intensive process. We find that some of this work could be automated, and implementing such automation may facilitate the development of future extensions to the psi-calculi framework.
|
|
| 8. |
- Wibling, Oskar
(author)
-
Ad hoc routing protocol validation
- 2005
-
Licentiate thesis (other academic/artistic)abstract
- We explore and evaluate methods for validation of ad hoc routing protocols which are used to set up forwarding paths in spontaneous networks of mobile devices. The focus is automatic formal verification but we also make an initial account of a protocol performance comparison using structured live testing. State explosion is a major problem in algorithmic verification of systems with concurrently executing components. We comment on some of the best reduction methods and their applicability to our work. For reactively operating ad hoc routing protocols we provide a broadcast abstraction which enables us to prove correct operation of the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) in scenarios of realistic size. Our live testing effort has thus far uncovered significant problems in the inter-operation between TCP and ad hoc routing protocols. Severe performance degradation results in networks of just a few nodes when very little mobility is introduced. This indicates that verification for smaller network sizes is also interesting since those configurations may be the only useful ones for certain types of applications.
|
|
| 9. |
- Åman Pohjola, Johannes
(author)
-
Bells and Whistles : Advanced language features in psi-calculi
- 2013
-
Licentiate thesis (other academic/artistic)abstract
- Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to every instance of the framework.The contribution of this licentiate thesis is to significantly extend the applicability and expressiveness of psi-calculi by incorporating several advanced language features into the framework: broadcasts, higher-order communication, generalised pattern matching, sorts and priorities. The extensions present several interesting technical challenges, such as negative premises. The machine-checked proofs for standard results about bisimilarity are generalised to each of these new settings, and the proof scripts are freely available online.
|
|
