Parallel Distributed Algorithm Design through Specification Transformation: The Asynchronous Vision System

1994
Article de conférence

Résumé

We present a constructive approach to the realization of a parallel system for the vision processing. This approach follows the classical software engineering principles: analysis, specification, design and implementation. The language CO-OPN (Concurrent Object Oriented Petri Net) is used to discribe the specification and the design of such system, while the implementation has been performed on a transputer machine. The writting of the CO-OPN specifications has been supported by the SANDS environement (Structured Algebraic Nets Development System) which also allow to simulate the behavior of the modelled system in an abstract way. A module, the main piece of the vision system, is presented that can be used for composing a computer vision architecture exploiting asynchronous data flows. This module is general enough to be duplicated and interconnected into a uniform graph. A module works by grouping asynchronous pieces of information coming through a channel, which delays them according to their relevance to the task of the module. The traditional separation between quantitative and symbolic processings vanishes since the module allows them to be implemented in a uniform way. The abstract specification of such principle is proposed, followed by a transformation refining this abstract specification into a concrete specification by introducing a distributed algorithm The concrete specification serves as the reference for the implementation on the distributed machine. We present a constructive approach to the realization of a parallel system for the vision processing. This approach follows the classical software engineering principles: analysis, specification, design and implementation. The language CO-OPN (Concurrent Object Oriented Petri Net) is used to discribe the specification and the design of such system, while the implementation has been performed on a transputer machine. The writting of the CO-OPN specifications has been supported by the SANDS environement (Structured Algebraic Nets Development System) which also allow to simulate the behavior of the modelled system in an abstract way. A module, the main piece of the vision system, is presented that can be used for composing a computer vision architecture exploiting asynchronous data flows. This module is general enough to be duplicated and interconnected into a uniform graph. A module works by grouping asynchronous pieces of information coming through a channel, which delays them according to their relevance to the task of the module. The traditional separation between quantitative and symbolic processings vanishes since the module allows them to be implemented in a uniform way. The abstract specification of such principle is proposed, followed by a transformation refining this abstract specification into a concrete specification by introducing a distributed algorithm The concrete specification serves as the reference for the implementation on the distributed machine.

Official source

https://infoscience.epfl.ch/record/54524?ln=fr

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés

Chargement

Publications associées

Chargement

1994
Article de conférence

Résumé

Official source

https://infoscience.epfl.ch/record/54524?ln=fr

À propos de ce résultat

Concepts associés (12)

Concepts associés

Chargement

Publications associées (11)

Publications associées

Chargement

SANDS is a development tool based on structured algebraic nets. The environment is composed of the following features: - Algebraic nets allowing the definition and use of structured tokens by means of algebraic specifications. Apart from reducing the size of a model these nets are accurate in describing data transformations during the evolution of the system being modelled; - Structured nets necessary for large system developments. The latter two components form together the language used and understood by the environment. The development environment provides the user with an application simulation tool. This component provides immediate views of any modifications brought to the system being modelled. The environment also permits modifications to the automatically generated code through manual insertions or deletions of C or Prolog instructions. Model semantics possess a well formalized underlying theory. Connections with other theories are numerous and offer a large range of possibilities for describing and proving properties about systems. We can mention amongst other rewriting systems, bisimulation (behaviour comparison between two system models), refinement of objects, algebraic specifications and proof of temporal logic properties used as a more abstract specification language. The user builds and structures his model as a set of algebraic nets called 'objects' representing either instances or classes depending on the context of the modelling. These objects are related to each other by synchronization links which determine and limit the way the objects can evolve concurrently. Algebraic specifications and objects can be used in three different ways: they can be generic, 'ground' or instantiated. The underlying model, namely CO-OPN (Concurrent Object-Oriented Petri Nets), is described in more depth in: 'CO-OPN: A Concurrent Object- Oriented Petri Nets' International Conference on Application and Theory of Petri Nets, Aarhus June 1991. SANDS has two main components: the CO-OPN graphical editor and the simulation tool. Both parts are independent in the following sense: the user can develop his model inside the graphical editor and call the simulation tool from the editor, on the other hand he can use the CO-OPN specification language to describe his model in a textual way and then use the simulation tool after having verified the validity of the specification with the compiler. Moreover these possibilities can be mixed. The user can also modify the specifications by editing the file generated by the graphical editor (written in the CO-OPN language). The graphical tool can be avoided, if desired, through hand written specifications describing the model; a specification made in the CO-OPN language can also be loaded and then modified in the graphical environment. The specifications obtained can then be simulated once the compilation and linking phases have been successfully achieved. The compiling and linking can be performed through the grap The algebraic specification of data can be defined outside of the graphical editor environment. When this has been done the latter specifications can be imported in the graphical editor where their signatures are graphically represented. This set of algebraic specifications are used as a basis which support object specifications. There is no constraint on the way the user builds his specifications. He can adopt a top-down or a bottom-up methodology. Therefore the user can set the overall objects distribution in order to structure his model and then define the behaviour of each object. On the othe hand he can build his application on a set of objects already defined. However, these approaches can also be mixed.

1993

Chargement

An incremental prototyping methodology for distributed systems based on formal specifications

This thesis presents a new incremental prototyping methodology for formally specified distributed systems. The objective of this methodology is to fill the gap which currently exists between the phase where a specification is simulated, generally using some sequential logical inference tool, and the phase where the modeled system has a reliable, efficient and maintainable distributed implementation in a main-stream object-oriented programming language. This objective is realized by application of a methodology we call Mixed Prototyping with Object-Orientation (in short: OOMP). This is an extension of an existing approach, namely Mixed Prototyping, that we have adapted to the object-oriented paradigm, of which we exploit the flexibility and inherent capability of modeling abstract entities. The OOMP process proceeds as follows. First, the source specifications are automatically translated into a class-based object-oriented language, thus providing a portable and high-level initial implementation. The generated class hierarchy is designed so that the developer may independently derive new sub-classes in order to make the prototype more efficient or to add functionalities that could not be specified with the given formalism. This prototyping process is performed incrementally in order to safely validate the modifications against the semantics of the specification. The resulting prototype can finally be considered as the end-user implementation of the specified software. The originality of our approach is that we exploit object-oriented programming techniques in the implementation of formal specifications in order to gain flexibility in the development process. Simultaneously, the object paradigm gives the means to harness this newly acquired freedom by allowing automatic generation of test routines which verify the conformance of the hand-written code with respect to the specifications. We demonstrate the generality of our prototyping scheme by applying it to a distributed collaborative diary program within the frame of CO-OPN (Concurrent Object-Oriented Petri Nets), a very powerful specification formalism which allows expressing concurrent and non-deterministic behaviours, and which provides structuring facilities such as modularity, encapsulation and genericity. An important effort has also been accomplished in the development or adaptation of distributed algorithms for cooperative symbolic resolution. These algorithms are used in the run-time support of the generated CO-OPN prototypes.

EPFL1997

Chargement

Formal testing of object-oriented software

Cécile Peraire

This thesis presents a method and a tool for test set selection, dedicated to object-oriented applications and based on formal specifications. Testing is one method to increase the quality of today's extraordinary complex software. The aim is to find program errors with respect to given criteria of correctness. In the case of formal testing, the criterion of correctness is the formal specification of the tested application: program behaviors are compared to those required by the specification. In this context, the difficulty of testing object-oriented software arises from the fact that the behavior of an object does not only depend on the input values of the parameters of its operations, but also on its current state, and generally on the current states of other related objects. This combinatorial explosion requires carefully selecting pertinent test sets of reasonable size. This thesis proposes a formal testing method which takes this issue into account. Our approach is based on two different formalisms: a specification language well adapted to the expression of system properties from the specifier's point of view, and a test language well adapted to the description of test sets from the tester's point of view. Specifications are written in an object-oriented language, CO-OPN (Concurrent Object-Oriented Petri Nets), based on synchronized algebraic Petri nets and devoted to the specification of concurrent systems. Test sets are expressed using a very simple temporal logic, HML (Hennessy-Milner Logic), whose logic formulas can be executed by a program. There exists a full agreement, shown in this thesis, between the CO-OPN and HML satisfaction relationships: the program satisfies its specification if and only if it satisfies the exhaustive test set derived from this specification. The exhaustive test set expresses all the specification properties. The exhaustive test set is generally infinite. Its size is reduced by applying hypotheses to the program behavior. These hypotheses define test selection strategies and reflect common test practices. The quality of the test sets thus selected only depends on the pertinence of the hypotheses. Concretely, the reduction is achieved by associating to each hypothesis applied to the program, a constraint on the test set. Our method proposes a set of elementary constraints: syntactic constraints on the structure of the tests and semantic constraints which allow to instantiate the test variables so as to cover the different classes of behaviors induced by the specification (subdomain decomposition). Elementary constraints can be combined to form complex constraints. Finally, the constraint system defined on the exhaustive test set is solved, and the solution leads to a pertinent test set of reasonable size. Thanks to the CO-OPN semantics, which allows to compute all the correct and incorrect behaviors induced by a specification, our method is able to test, on the one hand that a program does possess correct behaviors, and on the other hand that a program does not possess incorrect behaviors. An advantage of this approach is to provide through the tests, an observational description of valid and invalid implementations. Our testing method exhibits the advantage of being formal, and thus allows a semi-automation of the test selection process. A new tool, called CO-OPNTEST, is presented in this thesis. This tool assists the tester during the construction of constraints to apply to the exhaustive test set; afterward it automatically generates a test set satisfying these constraints. The CO-OPNTEST architecture is composed of a PROLOG kernel and a Java graphical interface. The kernel is an equational resolution procedure based on logic programming. It includes control mechanisms for subdomain decomposition. The graphical interface allows a user-friendly definition of the test constraints. The CO-OPNTEST tool has generated test sets for several case studies in a simple, rapid and efficient way. In particular, it has generated test sets for an industrial case study of realistic size: the control program of a production cell [Lewerentz 95]. CO-OPNTEST and its application to significant examples demonstrate the pertinence of our approach.

EPFL1998

Chargement

1993

An incremental prototyping methodology for distributed systems based on formal specifications

EPFL1997

Formal testing of object-oriented software

Cécile Peraire

EPFL1998