Logic, Computation and Rigorous Methods

System engineering development processes rely on modelling activities that lead to different design models corresponding to different analyses of the system under consideration.

A computably enumerable (c.e.) set A is mitotic if it can be split into two c.e. sets \(A_0\) and \(A_1\) which are Turing equivalent to A. Glaßer et al. [3] introduced two variants of this notion. The first variant weakens mitoticity by not requiring that the parts \(A_0\) and \(A_1\) of A are c.e., the second strengthens mitoticity by requiring that the parts \(A_0\) and \(A_1\) are computably separable. Glaßer et al. [3] raised the question whether these variants are nonequivalent to the classical mitoticity notion. Here we answer this question affirmatively. We also show, however, that the weaker mitoticity property is trivial, i.e., that any c.e. set has this property. Moreover, we consider and compare these new variations of mitoticity for the common strong reducibilities in place of Turing reducibility. Finally - not directly related to these results - we show that all weak truth-table (wtt) complete sets are wtt-mitotic, in fact strongly wtt-mitotic.

In view of the increasing importance of cyber-physical systems, and of their correct design, the Abstract State Machine (ASM) framework is extended to include continuously varying quantities as well as the conventional discretely changing ones. This opens the door to the more faithful modelling of many scenarios where digital systems have to interact with the continuously varying physical world. Transitions in the extended framework are thus either moded (catering for discontinuously changing quantities), or pliant (catering for smoothly changing quantities). An operational semantics is provided, first for monolithic systems, and this is then extended to give a semantics for systems consisting of several distinct subsystems. This allows each subsystem to undergo its own subsystem-specific mode and pliant transitions. Refinement is elaborated in the extended context for both monolithic and composed systems. The formalism is illustrated using an example of a bouncing tennis ball.

Stepwise design of programs is a divide-and-conquer strategy to control complexity in program modularization and theorems. It has been studied extensively in the last 30 years and has worked well, although it is not yet commonplace. This paper explores a new area of research, finding efficient products in colossal product spaces, that builds upon past work.

An important concept for nonmonotonic reasoning in the context of a conditional belief base \(\mathcal R\) is syntax splitting, essentially stating that taking only the syntactically relevant part of \(\mathcal R\) into account should be sufficient. In this paper, for the semantics of ordinal conditional functions (OCF) of \(\mathcal R\), we introduce the notion of semantic splitting of \(\mathcal R\) where the combination of models of sub-belief bases of \(\mathcal R\) corresponds to the models of \(\mathcal R\). While this is not the case for all OCF models, we show that for c-representations which are a subclass of all OCFs governed by the principle of conditional preservation, every syntactic splitting is also a semantic splitting. Furthermore, for the semantics of c-representations, we introduce constraint splittings of a conditional belief base and show that they fully capture and go beyond syntax splittings, thus allowing for additional belief base splittings that enable the computation of models locally from sub-belief bases.

In this paper, we discuss the community associated with Abstract State Machines (ASM), especially in the context of a Community of Practice (CoP), a social science concept, considering the development of ASM by its community of researchers and practitioners over time. We also consider the long-term historical context of the advisor tree of Egon Börger, the main promulgator of the ASM approach, which can be considered as multiple interrelated CoPs, distributed over several centuries. This includes notable mathematicians and philosophers among its number with some interesting links between the people involved. Despite most being active well before the inception of computer science, a number have been influential on the field.

“The bride is dressed in red and the groom in white.” Sometimes someone cannot believe their own ears, thinking they have misunderstood, and instead the communication is clear and exact, Egon actually got married in white and Donatella was in red. Some other times someone believe they have understood and instead the message is ambiguous and unclear.

When considering software requirements, one way to eliminate inaccuracies is to build a ground model and give it a formalization. In this paper, we propose an approach that begins by searching for terms and constructs that may cause communication problems and suggests a systematic way to disambiguate them.

In this paper we use the Abstract State Machine (ASM) method for high-level system design and analysis created by Egon Börger to formally specify Grover’s quantum database search algorithm, stepwise refining it from its highest abstraction level down to its implementation as a quantum circuit. Our aim is to raise the question of whether the ASM method in general and quantum ASMs in particular can improve the current practices of quantum system engineering; providing accurate high-level modelling and linking the descriptions at the successive stages of quantum systems development through a chain of rigorous and coherent system models at stepwise refined levels of abstraction.

The B landscape can be confusing to formal methods outsiders, especially due to the fact that it is partitioned into classical B for software and Event-B for systems modelling. In this article we shed light on commonalities and differences between these formalisms, based on our experience in building tools that support both of them. In particular, we examine not so well-known pitfalls. For example, despite sharing a common mathematical foundation in predicate logic, set theory and arithmetic, there are formulas that are true in Event-B and false in classical B, and vice-versa.

I sketch what I think led to the emergence of Abstract State Machines. A central role in this is played by the work of Ashok Chandra and David Harel on computable queries in databases. I also define Chandra-Harel Algebras, and analyse Blum-Shub-Smale computability over these algebras.

We define MOTION (MOdeling and simulaTIng mObile ad-hoc Networks), a Java application based on the framework ASMETA (ASM mETAmodeling), that uses the ASM (Abstract State Machine) formalism to model and simulate mobile networks. In particular, the AODV (Ad-hoc On-demand Distance Vector) protocol is used to show the behaviour of the application.

Abstract State Machines work with algorithms on the natural abstraction level. In this paper, we discuss the notion of the natural abstraction level of an algorithm and how ASM manage to capture this abstraction level. We will look into three areas of algorithms: the algorithm execution, the algorithm description, and the algorithm semantics. We conclude that ASM capture the natural abstraction level of the algorithm execution, but not necessarily of the algorithm description. ASM do also capture the natural abstraction level of execution semantics.

Safety-critical systems require development methods and processes that lead to provably correct systems in order to prevent catastrophic consequences due to system failure or unsafe operation. The use of models and formal analysis techniques is highly demanded both at design-time, to guarantee safety and other desired qualities already at the early stages of the system development, and at runtime, to address requirements assurance during the system operational stage.

In this paper, we present the modeling features and analysis techniques supported by ASMETA (ASM mETAmodeling), a set of tools for the Abstract State Machines formal method. We show how the modeling and analysis approaches in ASMETA can be used during the design, development, and operation phases of the assurance process for safety-critical systems, and we illustrate the advantages of integrated use of tools as that provided by ASMETA.

The Flashix project has developed the first realistic verified file system for Flash memory. This paper gives an overview over the project and the theory used. Specification is based on modular components and subcomponents, which may have concurrent implementations connected via refinement. Functional correctness and crash-safety of each component is verified separately. We highlight some components that were recently added to improve efficiency, such as file caches and concurrent garbage collection. The project generates 18K of C code that runs under Linux. We evaluate how efficiency has improved and compare to UBIFS, the most recent flash file system implementation available for the Linux kernel.

Over the last decades the field of computer science has changed a lot. In practice we are now dealing with very complex systems, but it seems that the theoretical foundations have not caught up with the development. This article is dedicated to a demonstration how a modernised theory of computation may look like. The theory is centred around the notion of algorithmic systems addressing behavioural theory, logic and complexity theory.

The domain of Subject-oriented Business Process Management (S-BPM) is somewhat outstanding due to its embracing of Subject Orientation. However, at the same time, it is also a classic BPM domain concerned with typical aspects like creation and exchange of diagrammatic process models, elicitation of domain knowledge, and implementing process (models) into organisations and IT systems. Nevertheless, the Abstract State Machine (ASM) concept, a formal and abstract specification means for algorithms, has been and is fundamental and an important cornerstone for the S-BPM community. The first formal specifications for S-BPM has been developed by Egon Börger using ASM means—namely a specification for an interpreter engine for the subject-oriented modeling language PASS, the Parallel Activity Specification Schema. However, for the sake of intuitive and comprehensive use, ASM can be enriched with defining the passive aspects of PASS, namely the (data) structure of process models and data object appearing in the processes. Here it is useful to complement ASM description means with concepts that are better suited for that tasks. This work analyzes how the S-BPM research community has combined ASM with the Web Ontology Language (OWL) to generate a precise, while comprehensible, system specification for the execution of formal, subject-oriented process models. Furthermore, it will be argued why this combination is worthwhile overcoming the weaknesses of both generic and technology independent specification approaches.

Models are a universal instrument of mankind. They surround us our whole lifespan and support all activities even in case we are not aware of the omnipresence. They are so omnipresent that we don’t realise their importance. Computer Science is also heavily using models as companion in most activities. Meanwhile, models became one of the main instruments. The nature and anatomy of models is not yet properly understood.

Computer Science research has not yet been properly investigating its principles, postulates, and paradigms. The well-accepted three dimensions are states, transformation, and collaboration. An element of the fourth dimension is abstraction. The fourth dimension is modelling. We review here the fourth dimension.

We present a framework for modeling the semantics of frequent concepts in the context of procedures and functions. In particular, we consider the concepts of recursive and non-recursive procedures, parameter passing mechanisms, return values, procedures as values (with local and non-local procedures), synchronous and asynchronous procedures, and for the latter, synchronization mechanisms. The concepts are mostly modeled in a combinable manner. Hence the concepts for procedures for many popular programming languages are covered by the framework.