The Hybrid Event-B framework was introduced to add continuously varying behaviour to the discrete changes of state characteristic of the well established Event-B method. This is made necessary by the needs of verifying the hybrid and cyber-physical systems that are increasingly prevalent today. The semantic foundation of Hybrid Event-B rests on piecewise absolutely continuous functions of time. This enables unproblematic modelling of all classical physical phenomena, as well as the specification of conventional discrete changes of state, regardless of whether these arise in the physical arena or as abstractions of computational behaviour. In this paper, the large gap between arbitrary piecewise absolutely continuous functions, and what can be reasoned about mechanically/symbolically, is addressed. First, piecewise absolutely continuous real functions are restricted to piecewise complex analytic functions, real and without singularities on a semi-infinite portion of the real axis. This class has good properties with respect to symbolic manipulation and thus provides a good foundation for an approach to system verification that avoids dealing with the interleaved quantifiers of mathematical analysis, thus reducing the verification of the proof obligations of Hybrid Event-B to calculational checks. The individual proof obligations, whose discharge assures the correctness of a Hybrid Event-B machine, are examined, and results establishing sufficient conditions for their successful discharge via calculation are given. A small scale case study illustrates the verification process in this setting.

Refinement of formal system models towards implementation has been a mainstay of system development since the inception of formal and Correct by Construction approaches to system development. However, pure refinement approaches do not always deal fluently with all desirable system requirements. This prompted the development of alternatives and generalizations, such as retrenchment. The crucial concept of simulation is key to judging the quality of the conformance between abstract and more concrete system models. Reformulations of these theoretical approaches are reprised and are embedded in a graded framework. The added flexibility this offers is intended to deal more effectively with the needs of applications in which the relationship between different levels of abstraction is not straightforward, and in which behavior can oscillate between conforming quite closely to an idealized abstraction and deviating quite far from it. The framework developed is confronted with an intentionally demanding case study: a model active control system for the protection of buildings during earthquakes. This offers many challenges: it is hybrid/cyber-physical; it has to respond to rather unpredictable inputs; and it has to straddle the gap between continuous behavior and discretized/quantized/numerical implementation.

The cyber-physical system (CPS) is a dynamic system that contains both continuous and discrete behaviors. It has a wide range of applications in fields such as health care equipment, intelligent traffic control and environmental monitoring. However, the combination of continuous physical behavior and discrete control behavior may complicate the design of systems further. It is of great necessity to give an explicit formal language and its semantics for CPS. In this paper, we elaborate the modeling language for CPS based on our previous work. This language supports shared variables to model the interaction between the physical and the cyber. Additionally, we give it denotational semantics and algebraic semantics, especially focus on the continuous behavior and its composition with the discrete behavior. Throughout this paper, we also present some examples to illustrate the feasibility of the language and its semantics.

Summary The Bitcoin model originated blockchain architectures and inspired their further development. Blockchain architectures are still most commonly associated with currency applications, and with financial speculation. Bitcoin's rewards forProof of Workmining became the default consensus technique for blockchains. As an alternative torewardmechanisms for blockchain maintenance, we proposepunishmentmechanisms for neglecting to maintain the blockchain (provided participants are intrinsically motivated to be beneficiaries of the blockchain application). Punishment not Reward is convincing for enterprise mission critical blockchain applications, and potential punishment mechanisms includedenial of serviceand/orrevocation of confidentiality. This obviates the need for reward via cryptocurrencies, along with their attendant volatility, insecure ecosystem, and market manipulation demerits. The privacy concerns of competing entities participating in a blockchain application areprima faciein conflict with the needs of the community to be able to inflict punishment mechanisms. Conflicts of this kind can be addressed via sophisticated cryptographic techniques such as secret sharing, multiparty computation, zero‐knowledge proofs, and so on, which play a vital role. We stress the importance of correctly balancing allapplication specificinterests in the engineering of blockchain applications, so that the mix of incentives and disincentives is stabilizing.

Abstract INSPEX is anINtegrated Smart sPatial EXplorationsystem. It relies on a family of sensors, like automated vehicles do, to provide enough information to a digital system for it to make reliable inferences about the location of obstacles and other impediments in its environment. Unlike the automated vehicle case, INSPEX is minaturised, because it is intended for lightweight applications and for portable use by humans, for example, visually impaired persons navigating outdoors (among many similar use cases). The complexity of this hardware‐focused system merited the introduction of formal methods during its (essentially conventionally structured) development. The aim was to improve the dependability of parts of the implemented system and to estimate system characteristics via modelling and calculation that could not be obtained experimentally within the scope of the project. The paper overviews the experience of the very much human‐in‐the‐loop use of formal techniques in the INSPEX Project and focuses particularly on the human issues that impacted the cooperation between the conventional techniques and formal methods.

Abstract In the effort to develop critical cyber‐physical systems, it is tempting to extend existing computing formalisms to include continuous behaviour. This may happen in a way that neglects elements necessary for correctly expressing continuous properties of the mathematics and correct physical properties of the real‐world physical system. A simple language is taken to illustrate these possibilities. Issues and risks latent in this kind of approach are identified and discussed under the umbrella of ‘healthiness conditions’. Modifications to the language in the light of the conditions discussed are elaborated, resulting in the language Combined Discrete and Physical Programmes in Parallel (CDPPP). An example air conditioning system is used to illustrate the concepts presented, and it is developed both in the original ‘unhealthy’ language and in the modified ‘healthier’ CDPPP. The formal semantics of the improved language is explored.

No abstract available.

The INSPEX project aims to miniaturize state-of-the-art obstacle detection technology comprising heterogeneous sensors and advanced processing, so that it can be used for wearable devices. The project focuses on enhancing the white cane used by some visually impaired and blind people. Due to high demand for reliability and performance, the project is a good candidate for the use of formal methods. In this paper, we report lessons we have learned from formal modelling exercises related to the pre-processing of sensor information in INSPEX.

The INSPEX H2020 project main objective is to integrate automotive-equivalent spatial exploration and obstacle detection functionalities into a portable/wearable multi-sensor, miniaturised, low power device. The INSPEX system will detect and localise in real-time static and mobile obstacles under various environmental conditions in 3D. Potential applications range from safer human navigation in reduced visibility, small robot/drone obstacle avoidance systems to navigation for the visually/mobility impaired, this latter being the primary use-case considered in the project.

A system development case study problem based on a set of aircraft landing gear is examined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). Although tool support for Hybrid Event-B is currently lacking, the complexity of the case study provides a valuable challenge for the expressivity and modelling capabilities of the Hybrid Event-B formalism. The size of the case study, and in particular, the number of overtly independent subcomponents that the problem domain contains, both significantly exercise the multi-machine and coordination capabilities of the modelling formalism. These aspects of the case study, vital in the development of realistic cyberphysical systems in general, have contributed significant improvements in the theoretical formulation of multi-machine Hybrid Event-B itself.

A case study centred on a fuel supply system for a small aircraft is presented in Hybrid Event-B, an extension of conventional Event-B that allows for the modelling and verification of hybrid and cyberphysical systems exhibiting nontrivial continuous behaviour. In contrast to many such case studies, which concentrate predominantly on timing issues, the focus in the present work is on nontrivial physical behaviour, and on the effect that this has on various refinement and partition strategies.

In conventional formal model based development frameworks, invariants play a key role in controlling the behaviour of the model (when they contribute to the definition of the model) or in verifying the model's properties (when the model, independently defined, is required to preserve the invariants). However, when variables take values distributed according to some probability distribution, the possibility of verifying that system behaviour is, in the long term, confined to some acceptable set of states can be severely diminished because the system might, in fact, with low probability fail to be thus confined. This short paper proposes martingales as suitable analogues of invariants for capturing suitable properties of non-terminating systems whose behaviour is with high probability good, yet where a small chance of poor behaviour remains. The idea is explored in the context of the well-known Event-B framework.

Cyberphysical systems, with their interdependence between physical behaviour and digital control, need insights from frequency domain control engineering, state space control engineering and discrete formal systems theory for their proper description. Neglecting any of these, results in descriptions that omit essential details. Hybrid Event-B is a formalism that enables all the relevant detail to be assimilated. A case study based on yaw control for the KURT e-vehicle is used as a testbed to explore the effective interaction between the various needed disciplines in exploring a specific design issue, the formalisation of yaw control discretization, using Hybrid Event-B.

Retrenchment is a flexible model evolution formalism that compensates for the limitations imposed by specific formulations of refinement. Its refinement-like proof obligations feature additional predicates for accommodating design data describing the model change. The best results are obtained when refinement and retrenchment cooperate, the paradigmatic scheme for this being the commuting square or tower, in which ‘horizontal retrenchment rungs’ commute with ‘vertical refinement columns’ to navigate through a much more extensive design space than permitted by refinement alone. In practice, the navigation is accomplished through ‘square completion’ constructions, and we present and prove a full suite of square completion theorems.

In real hybrid and cyber physical systems, noise is a onstant accompaniment to (and distraction from) the deterministic behaviour that is ideally desired. Nevertheless, most formalisms for such systems restrict to the deterministic realm. This also includes Hybrid Event-B, an extension of Event-B that caters for continuous behaviour as first class citizen. The incorporation of stochastic behaviour into Hybrid Event-B is investigated. Some essential elements of this enhancement are discussed, and a small case study is explored.

Abstract A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process compatible with standard model based refinement methodologies. Starting with a formalized requirements analysis using KAOS, an abstract model of the continuous system is created in the ASM formalism. This requires extensions of the KAOS and ASM formalisms, capable of dealing with quantities evolving continuously over real time, which are developed. After considering how the continuous system, described as a continuous control system in the state space framework, can be discretized, a discrete control system is created in the state space framework. This is re-expressed in the ASM formalism. The rigorous results on the relationship between continuous and discrete control system models that are needed to establish provable properties of the discretization, then become the ingredients of a retrenchment between continuous and discrete ASM models, and are thus fully integrated into the formal development. The discrete ASM model can then be further refined towards implementation.

The cardiac pacemaker system, proposed as a problem topic in the Verification Grand Challenge, offers a range of difficulties to address for formal specification, development, and verification technologies. We focus on the sensing problem, the question of whether the heart has produced a spontaneous heartbeat or not. This question is plagued by uncertainties arising from the often unpredictable environment that a real pacemaker finds itself in. We develop a time domain tracking approach to this problem, as a complement to the usual frequency domain approach most frequently used. We develop our case study in the continuous ASM (Abstract State Machine) formalism, which is briefly summarised, through a series of refinement and retrenchment steps, each adding new levels of complexity to the model.

Abstract The manual construction of fault trees for complex systems is an error-prone and time-consuming activity, encouraging automated techniques. In this paper we show how the retrenchment approach to formal system model evolution can be developed into a versatile structured approach for the mechanical construction of fault trees. The system structure and the structure of retrenchment concessions interact to generate fault trees with appropriately deep nesting. We show how this approach can be extended to deal with minimisation, thereby diminishing the post hoc subsumption workload and potentially rendering some infeasible cases feasible.

Abstract The retrenchment approach to the mechanical construction of fault trees, introduced in the first paper for combinational logic circuits, is extended to handle clocked circuits and then feedback circuits. The temporal behaviour of clocked circuits is captured using their causal relations, and the potentially unbounded behaviour of cyclic circuits is decomposed into an iteration over their acyclic counterparts. The repercussions of all this for the theory of retrenchment are elaborated. For clocked circuits, the techniques we present allow glitches and other transient errors to be properly described. For feedback circuits, the plethora of behaviours that can occur, give rise to infinitary fault trees of an appropriate kind. All this paves the way for automated fault tree generation for reactive systems.

Abstract The issues surrounding the question of atomicity, both in the past and nowadays, are briefly reviewed, and a picture of an ACID (atomic, consistent, isolated, durable) transaction as a refinement problem is presented. An example of a simple air traffic control system is introduced, and the discrepancies that can arise when read-only operations examine the state at atomic and finegrained levels are handled by retrenchment. Non-ACID timing aspects of the ATC example are also handled by retrenchment, and the treatment is generalised to yield the Retrenchment Atomicity Pattern . The utility of the pattern is confirmed against a number of different case studies. One is the Mondex Electronic Purse, its protocol treated as a conventional atomic transaction. Another is the recovery protocol of Mondex, viewed as a compensated transaction (leading to the view that compensated transactions in general fit the pattern). A final one comprises various unruly phenomena occurring in the implementations of software transactional memory systems, which can frequently display non-ACID behaviour. In all cases the Atomicity Pattern is seen to perform well.

Abstract UseCase-wise Development, an ‘Agile Method’ which introduces functionality into an application stage by stage, with each stage being carried through (ideally) to implementation before the next is considered, is examined with a view to its being treated via an Event-B methodology. The need to modify top level behaviour in a non-skip way precludes its naive treatment via Event-B refinement, and paves the way for the use of retrenchment in an Event-B context. An Event-B formulation of retrenchment aligned to the practicalities of the Rodin toolset is described. The details of refinement/retrenchment interworking needed to handle UseCase-wise development are outlined, and three small case studies are discussed. The details of the integration of the retrenchment proposal into Rodin are outlined.

Richard Banach; Review of Modeling in Event-B: System and Sofware Engineering, 1st edition, by Jean-Raymond Abrial, Journal of Logic and Computation, Volume 21,

Abstract Inspired by the properties of the refinement development of the Mondex Electronic Purse, we view an isolated atomic action as a family of transitions with a common before-state, and different after-states corresponding to different possible outcomes when the action is attempted. We view a protocol for an atomic action as a computation DAG, each path of which achieves in several steps one of the outcomes of the atomic action. We show that in this picture, the protocol can be viewed as a relational refinement of the atomic action in a number of ways. Firstly, it yields a ‘big diagram’ simulation à la ASM. Secondly, it yields a ‘small diagram’ simulation, in which the atomic action is synchronised with an individual step along each path through the protocol, and all the other steps of the path simulate skip. We show that provided each path through the protocol contains one step synchronised with the atomic action, the choice of synchronisation point can be made freely. We describe the relationship between such synchronisations and forward and backward simulations. We relate this theory to serialisations of system runs containing multiple interleaved transactions, showing how the clean picture of the refinement of an isolated atomic action to an isolated protocol becomes obscured by the details of the interleaving. In effect, the fact that protocols are typically executed by a number of co-operating agents, not all of which embark on executing the protocol at the same moment, results in ‘ragged starts’ and ‘ragged ends’ to protocol instantiations, leading to potential overlaps between unrelated protocol instances that the theory must handle. We show how existing Mondex refinements embody the ideas developed, and describe a mechanical verification of the results presented.

Retrenchment is a framework that allows relatively unrestricted system evolution steps to be described in a way that gives an evolution step some formal content - unlike model based refinement, whence it emerged, which is inapplicable outside some fairly tightly drawn notion of `progress towards implementation'. In this paper, we introduce a `coarse grained' version of retrenchment, relating to system behaviours in the large, and exemplify it on the requirements issues surrounding a denial of service case study drawn from the Mondex Purse. We show that the coarse grained retrenchment framework gives a good account of this case study.

The issues surrounding the question of atomicity, both in the past and nowadays, are briefly reviewed, and a picture of an ACID (atomic, consistent, isolated, durable) transaction as a refinement problem is presented. An example of a simple air traffic control system is introduced, and the discrepancies that can arise when read-only operations examine the state at atomic and finegrained levels are handled by retrenchment. Non-ACID timing aspects of the ATC example are also handled by retrenchment, and the treatment is generalised as the retrenchment Atomicity Pattern. The utility of the pattern is confirmed against a different case study, the Mondex Electronic Purse.

In model based formal methods, incompatible tools for different techniques is the norm. However, greater applicability to industrial scale systems increasingly requires combining the strengths of different techniques, in line with the verification grand challenge. The Frog tool embodies a construct-based specification syntax, and its meta-language Frog-CCL allows the generic configuration of both a constructs syntax and its proof obligations. For a specific system, Frog generates the system's verification conditions mechanically from the generic ones. Relationships between systems such as refinement and retrenchment can be configured. An example retrenchment between two simple systems illustrates the technique.

The Mondex Electronic Purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment tower pattern is used to address one such issue in detail: the use of a hash function rather than a total injective function when clearing the highly constrained purse logs. A retrenchment is constructed from the lowest level model to a model using a hash, and is then lifted to create two refinement developments, working at different levels of detail, and connected via retrenchments. The tower development is appropriately validated, vindicating the design used.

The various theories of model based refinement that have arisen over the years offer powerful methods of transforming abstract formal models into (what are ultimately) implementations, with a high degree of assurance that suitable properties of the abstract model have been preserved. Formal model based refinement has had considerable success in selected critical projects such as the Meteor Project for the Paris Metro and a number of smartcard based developments such as the Mondex Purse and the Javacard. However, refinement is very demanding as regards the precise relationship between abstract models and their more concrete counterparts, and these aspects can inhibit its use, or at least undermine its connection to system requirements

Retrenchment is a weakening of model based refinement that enables many development steps not expressible by refinement to be formally described nevertheless. The greater flexibility of retrenchment comes at the price of much feebler guarantees as compared with refinement, and so the interplay between retrenchment and refinement can hope to offer the best of both worlds. The paper explores the strategy of filtering the information in a retrenchment to yield a refinement under a suitable notion of observation. A general construction is given that enables a retrenchment, with its intrinsic notion of observability, to be filtered to produce a refinement with its intrinsic notion of observability. A simple running example illustrates the theory

The Mondex electronic purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment tower pattern is used to address one such issue in detail: the finiteness of the purse log (which records unsuccessful transactions). A retrenchment is constructed from the lowest level model of the purse system to a model in which logs are finite, and is then lifted to create two refinement developments of the purse, working at different levels of detail, and connected via retrenchments, forming the tower. The tower development is appropriately validated, vindicating the design used

Simple retrenchment is briefly reviewed in the B specification language of J.-R. Abrial (1996) as a liberalization of classical refinement, for the formal description of application developments too demanding for refinement. The looser relationships allowed by retrenchment between adjacent models in the development process may capture some of the requirements information of the development. This can make requirements validation more difficult to understand since the locus of requirements should be the models, and not their interrelationships, as far as possible. Hence the universal construction by Banach (2000), originally proposed for simple transition systems, is reformulated in B, in order to "lift" a given retrenchment conceptually, thus retracting such requirements information back to the level of abstraction of the abstract, ideal model. Examples demonstrate the cognitive value of retracting requirements to the abstract level, articulated in a well-understood formal language. This is also seen to yield a more understandable way of comparing alternative retrenchment designs. Some new B syntax in the pre- and postcondition style is presented to facilitate expression of the lifted requirements.

Review of Process Algebra with Timing by J. C. M. Baeten and C. A. Middelburg . Springer , 2002, ISBN 3-540-43447-X. £42

1University of Manchester Refinement in Z and object‐Z: Foundations and Advanced Applications John Derrick Eerke Boiten Springer‐Verlag 2001 £49.50 1‐85233‐245‐X

Journal Article Book Reviews Get access Journal of Logic and Computation, Volume 13, Issue 4, August 2003, Pages 625–627, https://doi.org/10.1093/logcom/13.4.625 Published: 01 August 2003

Review of Mathematics of Quantum Computation edited by Ranee K. Brylinski and Goong Chen . CRC Press , 2002. 448 ISBN 1584882824

Review of Handbook of Process Algebra edited by J. A. Bergstra, A. Ponse and S. A. Smolka . North-Holland Elsevier , 2001. 1356 EUR 177 . ISBN 0444828303

The more obvious and well known drawbacks of using refinement as the sole means of progressing from an abstract model to a concrete implementation are reviewed. Retrenchment is presented in a simple partial correctness framework as a more flexible development concept for formally capturing the early and otherwise preformal stages of development, and briefly justified. Given a retrenchment from an abstract to a concrete model, the problem of finding a model at the level of abstraction of the abstract model, but refinable to the concrete one, is examined. A construction is given that solves the problem in a universal manner, there being a canonical factorisation of the original retrenchment, into a retrenchment to the universal system followed by an I/O-filtered refinement. The universality amounts to the observation that the retrenchment component of any similar factorisation, factors uniquely through the universal model. The construction's claim to be at the right level of abstraction is supported by an idempotence property. The consequences of including termination criteria in the formal models is briefly explored.

Retrenchment is presented in a simple relational framework as a more flexible development concept than refinement for capturing the early preformal stages of development, and briefly justified. Fragmented retrenchment permits the granularity of actions to decrease across a development step, many concrete steps retrenching a single abstract one. This generates the usual proliferation of interleavings of events at the concrete level. Event structures, particularly flow event structures, help to control these within the retrenchments of a single abstract step, while the concurrent reading of the fragmented retrenchment proof obligation permits acceptable interleavings of retrenchments of different steps. It is observed that retrenchment allows the convenient description of unfair behaviours when fairness is not guaranteed.

Discusses a simple example that demonstrates various expressive limitations of the refinement calculus, and suggests a liberalization of refinement, called retrenchent, which supports an analogous formal development calculus. Useful concrete system behaviour can be specified outside the domain of pure refinement, and a case is made for fluidity between I/O and state components across the development step. A syntax and a formal definition are presented for retrenchment, which has some necessary properties for a formal development calculus: transitivity gives stepwise composition of retrenchments, while monotonicity w.r.t. the specification language constructors gives piecewise construction of retrenchments.

Abstract. Sharp retrenchment is introduced and brie y justified informally, as a liberalisation of refinement. In sharp retrenchment the relationship between an abstract operation and its concrete counterpart is mediated by extra predicates, allowing most particularly the description of non-refinement-like properties, and the mixing of I/O and state aspects in the passage between levels of abstraction. Sharp retrenchments are brie y contrasted with unsharp ones. Sharp retrenchments are shown to have a natural law of composition, and the way in which refinements may be viewed as sharp retrenchments is discussed. Modulated refinement is introduced as a version of refinement allowing mixing of I/O and state aspects, in order to facilitate comparison between sharp retrenchment and refinement, and various notions of simulation are considered in this context, specifically: stepwise simulation, the ability of simulator to mimic a sequence of execution steps of the simulatee; strong simulation, in which states and step labels are mapped independently between simulatee and simulator; and the refinement notion itself. Special cases of sharp retrenchment are shown to possess various subsets of these simulation properties, and the extent to which sharp retrenchments contain refinements within them is addressed. The details of the theory are worked out for the B-Method, though the applicability of the underlying ideas is not limited to just that formalism.

The Flagship project aims to produce a computing technology based on the declarative style of programming. A major component of that technology is the design for a parallel machine that can efficiently utilize the implicit parallelism in declarative programs. The computational models that expose this implicit parallelism are described, and an architecture designed to use it is outlined. The operational issues, such as dynamic load balancing, that arise in such a system are discussed, and the mechanisms being used to evaluate the architecture are described.>