Narrow Results

We study a novel representation of semiautomata, which is motivated by the method of trace-assertion specifications of software modules. Each state of the semiautomaton is represented by an arbitrary word leading to that state, the canonical word. The transitions of the semiautomaton give rise to a right congruence, the state-equivalence, on the set of input words of the semiautomaton: two words are state-equivalent if and only if they lead to the same state. We present a simple algorithm for finding a set of generators for state-equivalence. Directly from this set of generators, we construct a confluent prefix-rewriting system which permits us to transform any word to its canonical representative. In general, the rewriting system may allow infinite derivations. To address this issue, we impose the condition of prefix-continuity on the set of canonical words. A set is prefix-continuous if, whenever a word w and a prefix u of w are in the set, then all the prefixes of w longer than u are also in the set. Prefix-continuous sets include prefix-free and prefix-closed sets as special cases. We prove that the rewriting system is Noetherian if and only if the set of canonical words is prefix-continuous. Furthermore, if the set of canonical words is prefix-continuous, then the set of rewriting rules is irredundant. We show that each prefix-continuous canonical set corresponds to a spanning forest of the semiautomaton.

In the paper [1], Theorem 23 and Example 24 are incorrect. The corrected version is presented in this note.

In this paper, we propose a formal approach of Artificial Intelligence (AI) in securing object oriented database systems. We combine the specification of object oriented database with security policies and provide its formal syntax and semantics. The properties in the inheritance of authorizations in object oriented database system and reasoning about authorizations on data objects are also investigated in detail.

In a recent book, the author presented a mathematical specification of a blackboard system shell. The exercise suggested a method for developing blackboard systems with the aid of formal methods. This paper describes a formal method for the development of blackboard systems. The method is based, in part, on an informal one. Apart from the difference in emphasis (formal rather than informal), the new approach rests upon a formal definition of the architecture. The essential idea is that the mapping between the formal model of the problem domain (which is intended to be similar to the formal models proposed by, for example, Hayes) and the blackboard shell should be supported by formal proofs of correctness in a way identical to formal software engineering.

We present an informal method for constructing blackboard systems. The informal method forms the basis of the formal method whose initial stages are then described. We outline the formal treatment of control and suggest the use of temporal logic as a tool for reasoning about control. The paper ends with a review of the method.

Advances in VLSI technology make it possible to realize systems of very high complexity in a small volume of hardware using integration. In many application fields, it is necessary to implement certain algorithms, or even complete information processing systems, directly in silicon. Application domains which are likely to benefit are in the fields of signal processing and scientific computing.

In this paper, we consider several steps which we believe to be essential in the design path of a special purpose architecture, and we present methodologies for achieving design requirements. These solutions are based on experience gathered in the Parallel VLSI Architecture group of IRISA.

Multimedia systems incorporating hyperlinks and user interaction can be prototyped using TAOML, an extension of HTML. TAOML is used to define a Teleaction Object (TAO) which is a multimedia object with associated hypergraph structure and knowledge structure The hypergraph structure supports the effective presentation and efficient communication of multimedia information. In this paper, a formal specification methodology for TAOs using Symbol Relation (SR) grammars is described. An attributed SR grammar is then introduced in order to associate knowledge with the TAO. The limitations to achieve an efficient parser are given. The grammatical formalism allows for validation and verification of the system specification. This methodology provides a principled approach to specify, verify, validate and prototype multimedia applications.

Next generation information systems (NGISs) have to support the manipulation of data-oriented, behavioral and deductive aspects of application domains. Many modeling methods, e.g. UML and other object-oriented modeling methods offer primitives for modeling data-oriented and behavioral aspects but they do not support the modeling of deductive aspects. In addition, NGISs may be implemented by several separate software/database systems that are based on different paradigms. Therefore it is not appropriate to use such a modeling method which is based on one paradigm. In NGISs it is essential to integrate the value-oriented approach with the object-oriented approach. We develop a relational deductive object-oriented modeling (RDOOM) approach for NGISs. Our goal is to combine into one modeling method, the navigation power of the relational model, the modeling power of the object-orientation and the inference power of the deductive (logical) framework. It is obvious that in NGISs complex and large specifications have to be embedded in application-specific concepts and structures that are defined beforehand for users to facilitate their query formulation. The detection and specification of application-specific concepts and structures means a new challenge for analysis methods. We show that on the basis of the primitives of RDOOM it is possible to represent this kind of application-specific information in a natural way. It is also necessary that the appropriateness and adequacy of application-specific concepts and structures can be tested before their expensive design and implementation phases. For the definition of these concepts and structures a diagrammatic representation typical of many modeling methods is not sufficient. Rather, a precise and executable representation is needed. Especially the complex and large derivation rules behind deductive concepts cannot be expressed precisely with diagrammatic representations. We develop set-theoretical representations for our primitives. The precise representation of the result of systems analysis also gives a more substantial starting point for the design and implementation of NGISs.

Z is a formal specification language for describing sequential software systems. As the use of Z increases, the quality of Z specifications as effective means of communication arises. The aim of this paper is to contribute to a systematic assessment of the quality of Z specifications as perceived by their stakeholders. A pragmatic quality framework for Z specifications using notions from semiotics, cognitive psychology, and information system quality is proposed. The goals for pragmatic quality, and manageable criteria and mechanisms to address them in a feasible manner are identified. The utility and trade-offs of the mechanisms in achieving the quality goals of the framework are analyzed. Examples that lead to compromise of pragmatic quality in a Z specification, and techniques for improvement, are given.

Software development can be seen as a process of knowledge acquisition, in which human beings progressively learn about the intended behavior of the desired systems. Thereby, development is subject to considerable amounts of uncertainty and variability, that make it impossible to proceed in a purely incremental fashion — at some points, the need always arises to reconsider part of the accumulated knowledge. With this problem in mind, agile development methodologies have been gaining popularity in recent years as a means to enhance productivity, and there have been attempts to supplement them with formal techniques for better reliability. However, the existing approaches to agile formal methods have practically limited themselves to adopting recommended practices of agile development, with no particular contribution from the employed formalisms. Compared to that, this paper advocates the use of formalisms intended for evolutionary development, with a two-fold objective: first, to exploit the knowledge acquired up to any given stage as a means to cope with frequent and numerous changes; and, second, to introduce support for the creative development tasks through an interactive procedure that helps taking steps forward.

This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours.

Model Checking based verification techniques represent an important issue in the field of concurrent systems quality assurance. The lack of formal semantics in the existing formalisms describing multi-agents models combined with multi-agents systems complexity are sources of several problems during their development process. The Maude language, based on rewriting logic, offers a rich notation supporting formal specification and implementation of concurrent systems. In addition to its modeling capacity, the Maude environment integrates a Model Checker based on Linear Temporal Logic (LTL) for distributed systems verification. In this paper, we present a formal and generic framework (DIMA-Maude) supporting formal description and verification of DIMA multi-agents models.

One of the main ideas of agile development is to perform continuous integration, in order to detect and resolve conflicts among several modular units of a system as soon as possible. Whereas this feature is well catered for at the level of programming source code, the support available in formal specification environments is still rather unsatisfactory: it is possible to analyze the composition of several modular units automatically, but no assistance is given to help modify them in case of problems. Instead, the stakeholders who build the specifications are forced to attempt manual changes until reaching the desired functionality, in a process that is far from being intuitive. In response to that, this paper presents procedures and algorithms that automate the whole process of doing integration analyses and generating revisions to solve the diagnosed problems. These mechanisms serve to complete an agile specification environment presented in a previous paper, which was designed around the principle of facilitating the creative efforts of the stakeholders.

A mobile agent system is a special distributed system with moving programs in networks. Mobile agent systems provide a powerful and flexible paradigm for building high performance distributed systems. Due to dynamic configuration property, assuring quality of a mobile agent system is a challenge work. Formal specification and analysis of a mobile agent system provides one of the best approaches to ensure the correctness of a system design. However, it is difficult to find a formal specification tool for modeling a mobile agent system with an easy to understand and concise model. In addition, it is a challenge but also important work to provide an automatic formal analysis approach for verifying whether a system specification correctly meets certain requirements in a mobile agent system. In this paper, a framework for specification and analysis of mobile agent systems is defined. First, Predicate/Transition nets are extended with dynamic channels for modeling mobile agent systems. The formalism has the expressive power to naturally model the software architecture of a mobile agent system, and easily capture the properties especially the mobility, mobile communication and dynamic configuration of a mobile agent system. Then, model checking is instrumented to the framework for automatically verifying the correctness of the specification of a mobile agent system. In order to illustrate the capability of the formalism and the verification strategy, a medical image processing system using mobile agents is modeled using the extended Predicate/Transition nets and system properties are verified using the SPIN model checker.

Software risk comes mainly from its poor reliability, but how to effectively achieve high reliability still remains a challenge. This paper puts forward a framework for systematically integrating formal specification, review, and testing, and shows how it can be applied to effectively eliminate errors in the major phases of software development process to enhance software reliability. In this framework, requirements errors can be removed and missing requirements can be identified by formalizing requirements into formal specifications whose validity can be ensured by rigorous review. The valid specification can then be used as a firm foundation for implementation and for rigorous inspection, testing, and walkthrough of the implemented program. We discuss how formalization, review, and testing work together at different levels of software development to improve software reliability through detecting and removing errors in documentation.

In our previous work, we presented a Z-based formalism, called NZ, by which one can explicitly specify bounded, unbounded, erratic, angelic, demonic, loose, strict, singular, and plural nondeterminism. The NZ notation is mainly based on a new notion of operation schemas, called multi-schema. Since the operations of the Z schema calculus do not work on multi-schemas anymore, in this paper we augment NZ with a new set of schema calculus operations that can be applied on multi-schemas as well as ordinary operation schemas. To demonstrate the usability of the resulting formalism, we show how this formalism can assist to model game-like situations and concurrent systems as two well-known classes of nondeterministic systems.

Service-based software (SBS) modeling is considered as a promising way to develop high-quality service-based systems. One major challenge of this methodology is how to effectively utilize existing software services in the process of system modeling to ensure the reliability of the system while reducing the development cost. In this paper, we propose an evolutionary method for the formal specification construction of SBS to tackle this problem. Initial requirements are gradually transformed into a formal design specification through three steps during which existing services are discovered, filtered, selected and adopted. Candidate services are discovered through a keyword-based searching. Then the services are analyzed from both the structural and behavioral perspectives for filtering. A specification-based testing technique is exploited to rigorously determine which candidate services are finally selected. The selected services are incorporated into the formal design model of the system. We present a case study that was conducted for evaluating the usability of the method. We have also developed a prototype tool for supporting the method to be applied in practice.

With the growing in size and complexity of modern computer systems, the need for improving the quality at all stages of software development has become a critical issue. The current software production has been largely dependent on manual code development. Despite the slow development process, the errors introduced by the programmers contribute to a substantial portion of defects in the final software product. This paper investigates the synergy of generating code and assertion constraints from formal design models and use them to verify the implementation. We translate Z formal models into their OCL counterparts and Java assertions. With the help of existing tools, we demonstrate various checkings at different levels to enhance correctness.

Inspite of numerous research advancements made in recent years in the area of formal techniques, specification of real-time systems is still proving to be a very challenging and difficult problem. In this context, this paper critically examines state-of-the-art specification techniques for real-time systems and analyzes the emerging trends.

Cogito 1 is the first iteration of a Z-based integrated methodology and support system for formal software development. This paper gives an overview of the Cogito methodology and associated tools. Particular emphasis is placed on the way in which Cogito integrates the various phases of the formal development process and provides comprehensive tools support for all phases of development addressed by the methodology.

Formal specification languages provide assistance to solving the problem of high maintenance costs caused by ineffective communication of a system’s requirements. Using a sound mathematical basis, a formal specification language provides a precise and definitive system description that can serve as a binding contract. Additionally, the integration of the object-oriented paradigm with a formal specification language provides increased potential for software reuse, conceptually cleaner specifications and a framework for defining interfaces. To this end, there has been significant work done to extend existing specification languages to allow object-oriented specifications.

This paper provides a comparison of such object-oriented specification languages, specifically, those extending Z. The paper is organized into five major sections. After a brief introduction to the concepts of formal specification languages and Z, a simple library system is defined and used as an example throughout the paper. Each of the object-oriented specification languages is introduced and classified as either using Z in an object-oriented style or providing a true object-oriented extension of Z. For each language, the specification of the example library system is presented following a brief overview of the language’s features. An in-depth comparison is made of each of the languages which provide a true object-oriented extension of Z.