Search

A software formal specification is useful if and only if it is consistent or non-conflictive. However, checking the correctness or consistency of a formal specification is a difficult task. This paper proposes a method to prove its consistency or correctness by generating relevant theorem proofs. Checking the correctness and consistency of Object-Z formal specification is the main goal, which can make the specifier to get confident. Because Object-Z has inheritance property, this paper discusses it from different aspects, and focuses on the reuse of theorem proof. Finally, theorem prover Z/EVES is used to analyze and verify the Object-Z theorem proofs (semi-)automatically. [ABSTRACT FROM AUTHOR]

Uncertainty and imprecision play an important role in the specification and analysis of complex systems. Therefore, it is important to provide methodologies and tools to support the correct development of these systems. In this paper we present a new formalism, based on fuzzy automata, to facilitate the different phases involved in the development of a system where information is fuzzy. The formal syntax and semantics of our formalism are based on previous work, which has been adapted to be easily implemented and automated. We introduce a methodology to analyze systems modelled with one of our fuzzy automata. Finally, we show how our framework can be used to define a model of the heart based on electrocardiograms (ECGs) and use this model to analyze data of real patients. [ABSTRACT FROM AUTHOR]

Distributed fault localization, isolation and supply restoration (FLISR) algorithm only uses local topology information to improve system reliability in electric power enterprises. It has better adaptability than traditional centralized control architecture. To verify the correctness and reliability of the distributed FLISR algorithm which applied to complex distribution network is very important in the operation of distribution network. A formal method for the specification and verification of the distributed FLISR algorithm which uses linear temporal logic (LTL) language is presented in this paper. In addition, the correctness of the algorithm in interference-free situation and the security of the algorithm in some uncertain interference such as switch action failure, communication failure and other confounding factors are proved mathematically. [ABSTRACT FROM AUTHOR]

Fair input/output (or I/O) automata are a state-machine model for specifying and verifying reactive and concurrent systems. For the verification purposes, one is usually interested only in the sequences of interactions fair I/O automata offer to their environment. These sequences are called fair traces. The usual approach to the verification consists in proving fair trace inclusion between fair I/O automata. This paper presents a simple approach to the specification of fair traces and shows how to establish a fair trace inclusion relation for a pair of fair I/O automata by using the temporal logic of actions. [ABSTRACT FROM AUTHOR]

Modern day computer architectures offer ever-increasing support for parallel processing, still it turns out to be quite difficult for programmers and therefore programs to tap into these parallel resources. To benefit from real general-purpose parallel computing we claim that it is likely that a paradigm shift is needed in the way we think about programming. This change of thought in turn will need to be reflected in future programming languages as well. We think that the field of process algebra provides thorough insight in how to reason about the construction of software for concurrent systems and will be one of the enabling technologies supporting this transition. The wish to connect process algebra, a mathematical theory, to the world of computer-readable and executable specifications led to the development of PSF (Process Specification Formalism). PSF is an implementation of the process algebra ACP (Algebra of Communicating Processes) integrating ASF (Algebraic Specification Formalism) to specify algebraic data types. One of the first publications on PSF appeared in Fundamenta Informaticae in 1990. Here we stated as the first sentence of the abstract: "Traditional methods for programming sequential machines are inadequate for specifying parallel systems". Unfortunately, though some advancements have been made since 1990, we can still uphold this statement 20 years later. This current report documents the developments that lead to the construction of PSF and the 1990 publication and moreover it also documents how PSF and its tools have evolved since 1990 taking the conclusion and the outlook for future work from the original article as a reference point. Using the knowledge gained both in constructing tools for PSF and in using PSF to specify concurrent systems, we will judge, discuss and criticise the design decisions taken and show paths for future developments. [ABSTRACT FROM AUTHOR]

The DatagramCongestion Control Protocol (DCCP) is a new transport protocol standardized by the Internet Engineering Task Force (IETF) in March 2006. This paper discusses the specification of the connectionmanagement and synchronization procedures of DCCP using Coloured Petri Nets (CPNs). After introducing the protocol, we describe how the CPN model evolved as DCCP was being developed. We focus on our experience of incremental enhancement in the hope that this will provide guidance to those attempting to build complex protocol models. In particular, we discuss how the architecture, data structures and specification style of the model evolved as DCCP was developed. We finally recommend a procedure-based style once the standard is stable. The impact of this work on the DCCP standard and our interaction with IETF is also briefly discussed. [ABSTRACT FROM AUTHOR]

The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, unbounded, erratic, angelic, demonic, loose, strict, singular, and plural nondeterminism. To interpret our specifications, we use a constructive set theory, called CZ set theory, instead of the classical set theory Z. We have chosen CZ since it allows us to investigate the notion of nondeterminism from the formal program development point of view. In this way, we formally construct functional programs from Z specifications and then probe the effects of the initially specified nondeterminism on final programs. Our investigation shows that without specifying nondeterminism explicitly, the effects of the nondeterminism involved in initial specifications will not be preserved in final programs. We prove that using the new formalism, proposed by this paper, for writing nondeterministic specifications leads to programs that preserve the initially specified modalities of nondeterminism. [ABSTRACT FROM AUTHOR]

Today, users need to access their granted services from anywhere and at any time. Network security management must evolve to satisfy these requirements. The policy based network management approach proposes to separate the rules that govern the system from the functionalities provided by it. Nevertheless, the policy rules should be consistent, correct against the objectives and enforceable onto the devices. This problem becomes complex considering the dependencies of the rules – each rule on a device can impact another rule on another device – and each device needs specific configuration according to the technologies implemented. This article presents a formal framework for the refinement of network security management information. It includes three abstraction levels: the network security objectives, the network security tactics and the network security devices configurations. The information models of each abstraction level are formally specified and analysed (consistency, correctness and feasibility). A WBEM implementation of the formal refinement framework proves its feasibility in management architectures. [ABSTRACT FROM AUTHOR]

Many real-world systems can be conveniently modelled by the replication and interconnection of simple components of a few types: different configurations of the same system may vary just for the number of components and for the topology of their interconnections. In industrial practice of formal modelling the tedious work of such a manual instantiation has to be automated, allowing the inexpensive production of new configurations for the same product. This paper presents a methodology to build statechart models of topologically distributed systems by instantiating generic components; the method is able to replicate as needed statechart components and to expand the terms that drive their behaviour to create complex interconnection patterns along the required topology. The methodology is illustrated on the example of a classical distributed algorithm (Byzantine Agreement) in order to show the potential of dealing with parameterized distributed structures. The proposed methodology is shown to be able to find several interesting industrial applications. [ABSTRACT FROM AUTHOR]

In this paper, we present a formal and systematic approach allowing translating the specification of the interactions between agents, described using AUML formalism, in a Maude specification. Based on rewriting logic, the formal and object-oriented language Maude offers an interesting way for concurrent systems formal specification and programming. The main objectives of our approach are essentially: (1) to specify formally multi-agent systems behavior and, (2) to provide a healthy description preserving the consistency in their behavior and supporting their verification and validation process. The Maude descriptions, generated in the context of the developed framework, have been validated using the platform supporting the Maude language. [ABSTRACT FROM AUTHOR]

Component-Based Software Architecture is a promising solution for realizing distributed computing systems. To develop high quality software for such systems, an analysis of non-functional aspects of the software properties (also called Quality of Service or QoS) is very important. The UniFrame research project defines a Unified Meta-Component Model Framework (UniFrame) that includes a notion of QoS contracts. A classification of Quality of Service parameters, both static and dynamic, relevant to component-based distributed computing is developed and represented formally using Two-Level Grammar (TLG), an object-oriented formal specification language. TLG may be transformed into both a UML model, augmented with OCL constraints, and executable code in the Java programming language. This may be regarded as standardized code for implementation of the distributed application with dynamic measurement of the Quality of Service aspects incorporated. The approach is consistent with OMG's Model Driven Architecture (MDA) in that QoS properties may be specified at the Platform Independent Model (PIM) level and then carried down to the Platform Specific Model (PSM) level in implementation. [ABSTRACT FROM AUTHOR]