Abstract A natural encoding of synchronous message exchange with direct wait-control is proved to be equivalent in a distributed environment to a refinement which uses semaphores to implement wait control. The proof uses a most general scheduler, which is left as abstract and assumed to satisfy a few realistic, explicitly stated assumptions. We hope to provide a scheme that can be implemented by current theorem provers.
Abstract Despite the rich literature on network architecture and communication system design, the current practice of describing architectures remains informal and idiosyncratic. Such practice has evolved based on idiomatic terminology and hence, it is failing to provide a formal framework for representing and for reasoning about network architectures. This state of affairs has led to the overloading of architectural terms, and to the emergence of a large body of network architecture proposals with no clear indication of their cross similarities, their compatibility points, their unique properties, and their architectural performance and soundness. Formalizing network architectural descriptions is therefore a timely contribution, and this paper presents a first step in that direction. The paper builds upon architectural style modeling concepts from the software engineering field, and applies them to the network architecture space. Our approach is presented through a case study detailing a formal model for a common class of network architectures. The model uses a simple declarative language based on relations and first-order logic.
Abstract Many authors have drawn parallels between the relational model of data and the formal description technique Z, yet none of these contributions have managed to be both close to the relational model in terms of providing a practical means of database design and fully formal in terms of providing an appropriate metamodel. We compare these various formalisms, and suggest how the use of the formal template approach of Amálio et al might help to overcome some of the issues faced. We demonstrate the application of this work via a short case study, and suggest further enhancements to the template language.
Abstract The use of formal methods for software development is escalating over the period of time. The input to this formal specification phase is often the documents obtained during the requirements analysis activity which are either textual or semi-formal. Now there is a traceability gap between analysis and specification phases as verification of the semi-formal analysis model is difficult because of poor understandability of lower level of formalism of verification tools and validation of the formal specification is difficult for customers due to their inability to understand formal models. Our objective is to bridge this gap by a gradual introduction of formalism into the requirement model in order to facilitate its validation.We analyse our requirements with KAOS (Knowledge Acquisition in autOmated Specification) [1] which is a goal-oriented methodology for requirements modeling, then we translate the KAOS goal model, following our derived precise semantics [3], into an Event-B [2] formal specification, and finally we rigourously animate the obtained specification in order to validate its conformance to original requirements with the approach defined in [4].
Abstract Safety properties of a system may be specified by constraining the sequences of interactions of the system with its environment. This paper shows how to encode specifications in such a style using Alloy.
Abstract Few tools are available to help with the difficult task of validating that a Z specification captures its intended meaning. One tool that has been proven to be useful for validating specifications is the Alloy Analyzer, an interactive tool for checking and visualising Alloy models. However, Z specifications need to be translated to Alloy notation to make use of the Alloy Analyzer. These translations have been performed manually so far, which is a cumbersome and error-prone activity. The aim of this paper is to explore to what extent this process can be automated. The paper identifies a subset of Z that can be straightforwardly translated to Alloy, and the translation for this subset is formalised. More complex constructs, like schemas, are harder to translate. The paper gives a brief overview of the problems, and discusses alternative translation approaches.
Abstract Component-based software engineering is a practical approach to address the issue of building large software by combining existing and new components. However, building reliable software systems from components requires to verify the consistency of components and the correctness of their assemblies.