Modelling a Secure, Mobile and Transactional System with CO-OPN

Modelling complex concurrent systems is often difficult and error-prone, in particular when new concepts coming from advanced practical applications are considered. These new application domains include dynamicity, mobility, security, and localization dependent computing. In order to fully model and prototype such systems we propose to use several concepts introduced in our specification language CO-OPN, like context, dynamicity, mobility, subtyping and inheritance. CO-OPN (Concurrent Object Oriented Petri Net) is a formal specification language for modelling distributed systems; it is based on coordinated algebraic Petri nets. This paper focuses on the use of several basic mechanisms of CO-OPN for modelling mobile systems and the generation of corresponding Java code. A significant example of distributors accessible through mobile devices (for example, PDA with Bluetooth) is fully modelled and implemented with our technique.

Modelling a Secure, Mobile, and Transactional System with CO-OPN

Stanislav Chachkov

2003

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

SANDS: Structured Algebraic Net Development System

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

SANDS: Structured Algebraic Net Development System

1993

An incremental prototyping methodology for distributed systems based on formal specifications

EPFL1997