No abstract available.

Incident information sharing is being encouraged and mandated as a way of improving overall cyber intelligence and defense, but its take up is slow. Organisations may well be justified in perceiving risks in sharing and disclosing cyber incident information, but they tend to express such worries in broad and vague terms. This paper presents a specific and granular analysis of the risks in cyber incident information sharing, looking in detail at what information may be contained in incident reports and which specific risks are associated with its disclosure. We use the STIX incident model as indicative of the types of information that might be reported. For each data field included, we identify and evaluate the threats associated with its disclosure, including the extent to which it identifies organisations and individuals. The main outcome of this analysis is a detailed understanding of which information in cyber incident reports requires protection, against specific threats with assessed severity. A secondary outcome of the analysis is a set of guidelines for disciplined use of the STIX incident model in order to reduce information security risk.

Abstract This paper reconsiders refinements which introduce actions on the concrete level which were not present at the abstract level. It considers a range of different basic refinement relations, covering the standard ones for formalisms like Event-B, Z, action systems, and CSP. It also describes a number of ways in which new operations may be introduced: extended interfaces, internal actions, stuttering steps, and action refinement. The main contribution of this paper is in exploring the interaction between those two dimensions. In particular, it shows how the “refining skip” method is incompatible with failures-based refinement relations, and consequently some decisions in designing Event-B refinement are more entangled than previously highlighted.

No abstract available.

No abstract available.

Abstract Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.

No abstract available.

No abstract available.

No abstract available.

Abstract Two styles of description arise naturally in formal specification: state-based and behavioural. In state-based notations, a system is characterised by a collection of variables, and their values determine which actions may occur throughout a system history. Behavioural specifications describe the chronologies of actions—interactions between a system and its environment. The exact nature of such interactions is captured in a variety of semantic models with corresponding notions of refinement; refinement in state based systems is based on the semantics of sequential programs and is modelled relationally. Acknowledging that these viewpoints are complementary, substantial research has gone into combining the paradigms. The purpose of this paper is to do three things. First, we survey recent results linking the relational model of refinement to the process algebraic models. Specifically, we detail how variations in the relational framework lead to relational data refinement being in correspondence with traces–divergences, singleton failures and failures–divergences refinement in a process semantics. Second, we generalise these results by providing a general flexible scheme for incorporating the two main “erroneous” concurrent behaviours: deadlock and divergence, into relational refinement. This is shown to subsume previous characterisations. In doing this we derive relational refinement rules for specifications containing both internal operations and outputs that corresponds to failures–divergences refinement. Third, the theory has been formally specified and verified using the interactive theorem prover KIV.

No abstract available.

No abstract available.

Abstract Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable. Observations record, for example, which events a system is prepared to accept or refuse. Concurrent refinement relations include trace refinement, failures–divergences refinement, readiness refinement and bisimulation. Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of the input–output behaviour of abstract programs. These refinements are normally verified by using two simulation rules which help make the verification tractable. This paper unifies these two standpoints by generalising the standard relational model to include additional observable aspects. These are chosen in such a way that they represent exactly the notions of observation embedded in the various concurrent refinement relations. As a consequence, simulation rules for the tractable verification of concurrent refinement can be derived. We develop such simulation rules for failures–divergences refinement and readiness refinement in particular, using an alternative relational model in the latter case.

Abstract. This paper discusses the separation of components from the contexts in which they are used, and how this separation can be supported whilst using different specification languages. There are a number of ways in which this might be possible and here we show how the technique of promotion in Object-Z can be used to combine components which are specified using process algebras. We outline two approaches. The first is to separate out a single specification into a number of distinct viewpoints (i.e., partial specifications), each possibly written in a different notation. These viewpoints can be developed separately, but combined if necessary by a process of translation and unification. The alternative approach we discuss is to use a single hybrid language which is composed of a combination of notations, which we illustrate here by combining CSP and Object-Z. We illustrate both approaches with a simple example, and also consider how such component-based descriptions can be refined, which involves addressing the question of compositionality.

The 'viewpoint' approach, in which a system is described by several partial specifications, has been proposed as a way of making complex computing systems more understandable. The ISO's Open Distributing Processing (ODP) framework is an architecture for open distributed systems, involving five named viewpoints. This paper compares two partial specifications of a lending library-from the ODP's Enterprise and Information Viewpoints-and discusses the relation between them. Both specifications are written in Object-Z, an object-oriented variant of Z. Examining how such partial specifications might be unified raises broader issues of refinement and mutual consistency of partial specifications in Object-Z.

A specification provides a concise description of a system, and can be used as both the benchmark against which any implementation is tested, and also as a means to generate tests. Formal specifications have potential advantages over informal descriptions because they offer the possibility of reducing the costs of testing by automating part of the testing process. This observation has led to considerable interest in developing test generation techniques from formal specifications, and a number of different methods have been derived for state-based formalisms such as Z, B and VDM. However, after tests have been derived from a formal specification, the specification might be refined further before it is implemented, and therefore a mechanism is needed to relate the abstract tests to the refined implementation. The purpose of this paper is to provide such a method by exploring the relationship between testing and refinement. In this paper a model for test generation is used which constructs a finite state machine (FSM) from a Z specification by using a Disjunctive Normal Form (DNF) partition analysis of the state and operations. The finite state machine is then used to derive suitable test suites. The paper decribes a way of calculating an FSM for a refinement from an abstract FSM together with the information about the refinement embodied in the retrieve relation. This means that it is possible to test an implementation by generating a new concrete finite state machine from a set of abstract tests. Copyright © 1999 John Wiley & Sons, Ltd.

Abstract. An important aspect in the specification of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the interface to the environment (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. In this paper we are interested in the use of the formal specification notation Z for the description of distributed systems. Various conventions have been employed to model internal operations when specifying such systems in Z. If internal operations are distinguished in the specification notation, then refinement needs to deal with internal operations in appropriate ways. Using an example of a telecommunications protocol we show that standard Z refinement is inappropriate for refining a system when internal operations are specified explicitly. We present a generalisation of Z refinement, called weak refinement, which treats internal operations differently from observable operations when refining a system. We discuss the role of internal operations in a Z specification, and in particular whether an equivalent specification not containing internal operations can be found. The nature of divergence through livelock is also discussed.

The task of software production is to build software systems which are to fulfil certain requirements. For years the approach has been to build up by trial and error a program which, having satisfied carefully prepared test data, offers a plausible solution to the problem. But is it correct? Even for toy examples this is not obvious. In particular, it is often not even clear whether the original problem has been properly understood. The reason for this dilemma is that the transition from the informal problem statement to the final program is too big to be intellectually manageable. To master these problems, we advocate a software development method where the whole process is split into smaller steps by introducing formal specifications for (parts of) the problem and then stepwisely deriving efficient programs by correctness-preserving transformations.