49 research outputs found
Contexts, refinement and determinism
No full textIn this paper we have been influenced by those who take an “engineering view” of the problem of designing systems, i.e. a view that is motivated by what someone designing a real system will be concerned with, and what questions will arise as they work on their design. Specifically, we have borrowed from the testing work of Hennessy, de Nicola and van Glabbeek, e.g. [13, 5, 21, 40, 39].
Here we concentrate on one fundamental part of the engineering view and where consideration of it leads. The aspects we are concerned with are computational entities in contexts, observed by users. This leads to formalising design steps that are often left informal, and that in turn gives insights into non-determinism and ultimately leads to being able to use refinement in situations where existing techniques fail
Guarded operations, refinement and simulation
No full textSimulation rules have long been used as an effective computational means to decide refinement relations in state-based formalisms. Here we investigate how they might be amended so as to decide the event-based notion of singleton failures refinement of abstract data types or processes that have operations with a "guarded" interpretation. As the results presented here and found elsewhere in the literature are so sensitive to the details of the definitions used, we have machine-checked our results
Constructing programs or processes
No full textWe define interacting sequential programs, motivated originally by constructivist considerations. We use them to investigate notions of implementation and determinism. Process algebras do not define what can be implemented and what cannot. As we demonstrate it is problematic to do so on the set of all processes. Guided by constructivist notions we have constructed interacting sequential programs which we claim can be readily implemented and are a subset of processes
A robust semantics hides fewer errors
No full textIn this paper we explore how formal models are interpreted and to what degree meaning is captured in the formal semantics and to what degree it remains in the informal interpretation of the semantics. By applying a robust approach to the definition of refinement and semantics, favoured by the event-based community, to state-based theory we are able to move some aspects from the informal interpretation into the formal semantics
Bigraph Metaprogramming for Distributed Computation
No full textUbiquitous computing is a paradigm that emphasises integration of computing activities into the fabric of everyday life. With the increasing availability of small, cheap computing devices, the ubiquitous computing model seems more and more likely to supplant desktop computing as the dominant paradigm. Similarly, the presence of high-speed network connectivity between vast numbers of computers has already made distributed computing the preferred paradigm for many application domains. Unfortunately, traditional approaches to software development are not necessarily well-suited to developing software in a post-desktop world. We present an extension to the bigraphical reactive systems formalism that enables us to construct a programming language based upon it. We believe that this programming language provides programmers with an environment better suited to the challenges that arise when creating software within a distributed or ubiquitous computing paradigm. We detail our modification to the theory of bigraphical reactive systems that enables metaprogramming. Finally, we provide a description of our prototype implementation of a programming language that enables metaprogramming of bigraphical reactive systems
LSB - Live and Safe B: Alternative semantics for Event B
No full textWe define two lifted, total relation semantics for Event B machines: Safe B for safety-only properties and Live B for liveness properties. The usual Event B proof obligations, Safe, are sufficient to establish Safe B refinement. Satisfying Safe plus a simple additional proof obligation ACT REF is sufficient to establish Live B refinement. The use of lifted, total relations both prevents the ambiguity of the unlifted relational semantics and prevents operations being clairvoyant
General Refinement, Part Two: Flexible Refinement
No full textAbstractIn the previous, companion, paper [Reeves, S. and D. Streader, General refinement, part one: interfaces, determinism and special refinement, Proceedings of Refine 2008, Electronic Notes in Theoretical Computer Science (2008).] to this paper we introduced our general model of refinement, discussed ideas around determinism and interfaces that the general definition raised, and gave several examples showing how the general definition could be specialised to the sorts of refinement we see in the literature.In this paper we continue the story and we define vertical refinement on our general model. Vertical refinement can be seen as a generalisation of what, in the literature, has been called action refinement or non-atomic refinement. Alternatively, by viewing a special model (from the previous paper) as a logical theory, vertical refinement can be seen as a theory morphism, formalised as a Galois connection.We give an example of the utility of this definition by constructing a vertical refinement between broadcast processes and interactive branching programs, and we see how interactive branching programs can be implemented on a platform which provides broadcast communication.We also show how developments that fall outside the usual, special theories of refinement can be brought into the refinement world by giving examples of development which were thought not to be possible using refinement.Throughout, the central, simple idea of refinement as a development process that moves from abstract to concrete while preserving certain valuable guarantees will guide us
Atomic components
No full textThere has been much interest in components that combine the best of state-based and event-based approaches. The interface of a component can be thought of as its specification and substituting components with the same interface cannot be observed by any user of the components. Here we will define the semantics of atomic components where both states and event can be part of the interface. The resulting semantics is very similar to that of (event only) processes. But it has two main novelties: one, it does not need recursion or unique fixed points to model nontermination; and two, the behaviour of divergence is modelled by abstraction, i.e. the construction of the observational semantics
Stepwise refinement of processes
No full textIndustry is looking to create a market in reliable "plug-and-play" components. To model components in a modular style it would be useful to combine event-based and state-based
reasoning. One of the first steps in building an event-based model is to decide upon a set of atomic actions. This choice will depend on the formalism used, and may restrict in quite
unexpected ways what we are able to formalise. In this paper we illustrate some limits to developing real world processes using existing formalisms, and we define a new notion of refinement, vertical refinement, which addresses some of these limitations. We show that using vertical refinement we can rewrite specification into a different formalism, allowing us to move between handshake processes, broadcast processes and abstract data types
Modular synthesis of discrete controllers
No full textThis paper presents supervisory control theory in a process-algebraic setting, and proposes a way of synthesising modular supervisors that guarantee nonblocking. The framework used includes the possibility of hiding actions which results in nondeterminism. As modularity crucially depends on the process equivalence used, the paper studies possible equivalences and points out that, in order to be consistent with respect to the nonblocking property and to supervisor synthesis, a conflict-preserving equivalence must be used. It applies the results to synthesise nonblocking modular supervisors for a manufacturing system
