Abstract. This article is an introduction to Professor Howard Barringer, in honor of his 60th birthday on December 20, 2011, which was celebrated by the HOWARD-60 workshop (Higher-Order Workshop on Automated Runtime verification and Debugging), held on the same day at University of Manchester. |
Abstract. Though Timed CSP was developed 25 years ago and the CSP-based
refinement checker FDR was first released 20 years ago, there has never been
a version of this tool for Timed CSP. In this paper we report on the creation of
such a version, based on the digitisation results of Ouaknine} and
the associated development of discrete-time versions of Timed CSP with
associated models. |
Abstract. We present a systematic way of studying state machine based design spaces and apply it to the study of asynchronous pipelines. Starting with the specification of the most concurrent behaviour as a state machine, all possible valid smaller designs may be generated by systematically removing structured patterns of output states (C cuts) and input states (R cuts). Taking the cartesian product of cuts C X R yields the complete design space which may then be partitioned according to well understood design styles. In this paper we extend previous results by studying mixed asynchronous pipelines of which homogeneous behaviours form a subset. The approach is presented using the much smaller 2phase setting (3 X 6) but the insights and structures revealed carry over to full 4phase designs (35 X 140). We present a complete overview of mixed 2phase linear pipeline behaviours; show how their structuring C cuts and R cuts relate; characterise the behaviours of linear pipelines in terms of these cuts for any depth; and show how the much larger R mixed behaviour patterns can be calculated from knowledge of the C behaviour patterns. Applications of the theory cover mixed linear pipeline and ring behaviours and the automatic generation of quality circuits from our specifications. |
Abstract. We consider whether techniques from concurrency theory can be applied in the area of Cognitive Neuroscience. We focus on two potential applications. The first of these explores structural decomposition, which is effectively assumed by the localisation of function metaphor that so dominates current Cognitive Neuroscience. We take concurrency theory methods, especially Process Calculi, as canonical illustrations of system description notations that support structural decomposition and, in particular, encapsulation of behaviour. We argue that carrying these behavioural and notational properties over to the Cognitive Neuroscience setting is difficult, since neural networks (the modelling method of choice) are not naturally encapsulable. Our second application presents work on verifying stability properties of neural network learning algorithms using model checking. We thereby present evidence that a particular learning algorithm, the Generalised Recirculation algorithm, exhibits an especially severe form of instability, whereby it forgets what it has learnt, while continuing to be trained on the same pattern set. |
Abstract. "Up and Down the Temporal Way" was a paper published by Howard Barringer in the 1980s that used temporal logics to formally specify a lift system. Based on that temporal specification, we describe some advances and extensions to temporal specification and verification that the authors have been involved with since then. |
Abstract. Runtime validation techniques have been proposed as artifacts to detect and/or correct unforeseen behaviours of computer systems.
Their common features is to give only partial validation results, based on a restricted set of system executions produced in the real execution environment. A key issue is thus to better understand which kind of properties can (or cannot) be validated using such techniques.
We focus on three techniques known as runtime verification, property-oriented testing, and runtime enforcement. We present these approaches at an abstract level and in a unified framework, and we discuss their respective ability to deal with properties on infinite execution sequences, that are commonly encountered in many application domains. |
Abstract. This paper sets out the on-going research in a project which is
investigating how to learn from one interactive proof so that other similar proofs
can be completed automatically. |
Abstract. In this paper we present the notion of the Talmudic
Shkop extension to an abstract argumentation network (S,R) and compare it with Baroni’s
and his colleagues CF2 extensions and with Gabbay’s Equational approach to CF2 semantics.
We also offer tableaux methods as well as discuss temporal stamping of arguments and their use in resolving loops |
Abstract. We present a sound and complete model theory for theories of β-reduction with or without η-expansion. We then show in what conditions we obtain models of β-equality and βη-equality. |
Abstract. What are variables, and what is universal quantification over a variable?
Nominal sets are a notion of `sets with names', and using equational axioms in nominal algebra these names can be given substitution and quantification actions.
So we can axiomatise first-order logic as a nominal logical theory.
We can then seek a nominal sets representation theorem in which predicates are interpreted as sets; logical conjunction is interpreted as sets intersection; negation as complement.
Now what about substitution; what is it for substitution to act on a predicate-interpreted-as-a-set, in which case universal quantification becomes an infinite sets intersection?
Given answers to these questions, we can seek notions of topology.
What is the general notion of topological space of which our sets representation of predicates makes predicates into `open sets'; and what specific class of topological spaces corresponds to the image of nominal algebras for first-order logic?
The classic Stone duality answers these questions for Boolean algebras, representing them as Stone spaces.
Nominal algebra lets us extend Boolean algebras to `FOL-algebras', and nominal sets let us correspondingly extend Stone spaces to `∀-Stone spaces'.
These extensions reveal a wealth of structure, and we obtain an attractive and self-contained account of logic and topology in which variables directly populate the denotation, and open predicates are interpreted as sets rather than functions from valuations to sets. |
Abstract. We argue that a modern programming language such as Scala offers a level of succinctness, which makes it suitable for program and systems specification as well as for high-level programming. We illustrate this by comparing the language with the VDM++ specification language. The comparison also identifies areas where Scala perhaps could be improved, inspired by VDM++. We furthermore illustrate Scala's potential as a specification language by augmenting it with
a combination of parameterized state machines and temporal logic, defined as a library, thereby forming an expressive but simple runtime verification framework. |
Abstract. Model checking and runtime verification are pillars of formal verification but for the most part are used independently. In this position paper we argue that the formal verification community would be well-served by developing theory, algorithms, implementations, and applications that combine model checking and runtime verification into a single, seamless technology. This technology would allow system developers to carefully choose the appropriate balance between offline verification of expressive properties (model checking) and online verification of important parts of the system's state space (runtime verification). We present several realistic examples where such technology appears necessary and a preliminary formalization of the idea. |
Abstract. Quantitative verification techniques offer an effective means
of computing performance and reliability properties for a wide range of systems.
In many cases, it is necessary to perform repeated analyses of a system,
for example to identify trends in results, determine optimal system parameters
or when performing online analysis for adaptive systems.
We argue the need for incremental quantitative verification techniques
which are able to re-use results from previous verification runs in order to improve efficiency.
We report on recently proposed techniques for incremental quantitative verification of Markov decision processes,
based on a decomposition of the model into its strongly connected components.
We give an overview of the method, describe a number of useful optimisations
and show experimental results that illustrate significant gains in run-time performance
using the incremental approach. |
Abstract. An algebraic specification is viewed as a black box that rewrites input to a ``most basic'' canonical form. We argue that a canonical form should be given for each specific specification, to prevent ``cheating'' in the implementation. Furthermore, we argue that the definition of the canonical form may sometimes require semantic rather than syntactic information.
To relate an OO implementation to a specification requires opening the black box to some extent; we assess the choices to be made here. |
Abstract. Synthesis of control for distributed systems is considered to be undecidable problem, under the assumption that control is performed by supervisors syncrhonizing with the original processes and selectively blocking or supporting the enabled transitions. We describe a decidable distributed control problem, where additional communications are allowed between supervisors. In this way, we synthesize control for invariants, reachability, repeated reachability and parity conditions. Special attention is given to reducing the number of added communications. |
Abstract. In this note, we consider a notion of minimum model suitable for formulating a semantics of evolvable computing systems using a revision-based logic. We explore a range of proof systems for reasoning in the logic of minimum models and consider their application to the simulation of evolvable systems. Finally, we outline how these proof systems may be implemented in a logical framework. |
Abstract. Howard Barringer was a pioneer in the study of temporal logics with
fixpoints. Their addition adds considerable expressive power.
One general issue is how to define
proof systems for such logics. Here we examine proof systems for
modal logic with fixpoints. We present a tableau proof system
for checking validity of formulas
which uses names to keep track of unfoldings of fixpoint variables. |
Abstract. How do we engage with the artefacts that we build as software engineers or computer scientists? |
