1,721,019 research outputs found
Using Refinement to Analyse the Safety of an Authentication Protocol
No full textThis paper describes an approach to the analysis of security protocols using Abrial's B method. B is a general purpose formal method based on standard set theory and predicate logic. The refinement rule we use means that we only check for safety properties such as authentication rather than liveness properties such as absence of denial of service. The contribution of this paper is the development of a style of modelling and reasoning with B that allows for a straightforward and thorough analysis of security protocols. This analysis contributes to the understanding of a protocol and could lead to an improvement in the design of security protocols
Refinement of Dynamic Systems
No full textExisting refinement frameworks such as B allow a developer to specify a system on an abstract level. Subsequently, this abstract specification is refined into an implementation that performs the specified task. In this paper a conventional refinement approach is extended with a means for performance analysis. This new approach guides a developer towards well-performing implementations throughout the refinement process. The main achievement of this work is an elaboration of a connection between performance and trace refinement
Stepwise Refinement of Communicating Systems
No full textAbstractThe action system formalism [6] is a state-based approach to distributed computing. In this paper, it is shown how the action system formalism may be used to describe systems that communicate with their environment through synchronised value-passing. Definitions and rules are presented for refining and decomposing such action systems into distributed implementations in which internal communication is also based on synchronised value-passing. An important feature of the composition rule is that parallel components of a distributed system may be refined independently of the rest of the system. Specification and refinement is similar to the refinement calculus approach [4, 26, 28]. The theoretical basis for communication and distribution is Hoare's CSP [16]. Use of the refinement and decomposition rules is illustrated by the design of an unordered buffer, and then of a distributed message-passing system
- …
