L. Bonnet, L. Duchien, G. Florin, L. Seinturier
CNAM-Laboratoire Cedric
292, Rue St Martin, FR-75141 Paris Cedex 03e-mail {bonnet, duchien, florin, seintur}@cnam.fr
Key words: distributed applications, object-oriented methods, formal methods,distributed knowledge.
Abstract:
This paper outlines a new approach for specifying, proving, and implementingdistributed cooperative algorithms associated with an object-oriented design. Thereare many examples of distributed algorithms that can be implemented in this way(ordered multicast, routing, spanning tree construction, election, distributed garbagecollection). These algorithms present several peculiar aspects due to their parallel anddistributed environment. We propose to build a method that gathers three kinds oftools to specify and to prove distributed cooperative algorithms [2].1. Introduction
1.1. Formal methods aspects
In the field of software engineering, formal specifications and proofs helpdesigners to cope with the growing complexity of software applications preserving agood reliability level. Among the numerous existing formal methods that can beused, we choose the B method [1]. To summarize in few words its main features isdifficult. It mainly relies on refinement, set, and logic theory. As it is defined forsequential algorithms, this method must be extended and modified to cope with theparallel and distributed context.
One main characteristic of parallel and distributed algorithms is the existence ofpartial order relations that generally allow one to prove the correctness properties. Inthis way, to extend the B method for parallel and distributed applications isinteresting because of its set theory background. Indeed it allows easily one to defineand to use order relations between sets of objects, or sets of events or sets of actions.
So our first proposition is to represent the temporal logic aspects using orderrelations between actions. In our case (object-oriented design) we consider as theunderlying modal logic the Temporal Logic of Actions [8] where its operatorsË(always) and ◊ (eventually) can be expressed using order relations.1.2. Distributed Artificial Intelligence aspects
The second set of concepts comes from Distributed Artificial Intelligence(DAI). One main aspect of parallel and distributed computation is the uncertainty onknowledge of other sites (or agent) states. This is due either to transmission delays orto failures. Hence these performance or fault tolerance features must be correctlyconsidered. In our method, an epistemic logic approach is used to define knowledge(and belief) of sites [6]. It allows to model environments of entities, knowledgelevels, and groups behaviors.
Moreover, the behavioral reflexive approach of DAI (which is not until nowreally integrated in our work) could simplify the presentation of adaptive behaviors.These dynamic behaviors are needed to implement for example the adaptability toperformance modifications and to failures.1.3. The distributed algorithm aspects
Finally we are interested by some practical results of distributed algorithmsresearch. We use the general control structures developed for distributed algorithms(e.g. phased protocols, group remote procedure calls [3], recursive distributedprogramming or wave algorithms [5]). They can be powerfully gathered together tofacilitate the implementation of new solutions.2. Model of specification for cooperative system
The distributed object-oriented paradigm helps the designer to master thecomplexity of cooperative systems. To specify a distributed algorithm, we observe itfrom three points of view: the group of objects (a set of distributed entities involvedin a distributed computation), objects (a local entity), and their methods (an actionthat can be performed).
In our methodology we define an abstract machine specification as anequivalent state/transition model. A state is mainly characterized by its assertiondefinition. Such an assertion is first expressed using classical logic operators appliedto methods on remote or local objects. As it is stated in Section 1.2 we add otherlogic operators to include parallel and distributed features. They allow to expressknowledge and belief predicates. For the final implementation step these operatorsare realized by particular method calls. Finally a state predicate is verified if it takes avalue in a defined set of possible values. A transition is associated with an action tobe performed. In fact we use condition/action systems. An enabling condition for atransition is checked and, only if it is true, the corresponding action is executed.
Refinement transforms step by step an abstract model (in the remaining of thepaper we use invariably the terms specification and model) of a software system intoan executable code. It must be emphasized that, by our different refinement steps,each model inherits the behavioral and knowledge aspects from higher levels. Forinstance, when a knowledge predicate is used in a group specification, thecorresponding knowledge predicate will be found in the object specification level(for instance by the way of Boolean local variables).2.1. Group specifications
First, the group of objects specification level handles global states, or globalknowledge, and the global interactions between these objects to reach a given goal.So the highest level must define the chosen distributed strategy to solve the probleme.g. the global view of the distributed system behavior. The global interaction definesa collective action that corresponds to the coordination between the set of objects.The definition of this collective action can be complex. In distributed algorithms, weuse distributed global control structure as recursive waves, phased algorithms orgroup remote procedure calls as a complex global behavior. These different kinds ofstructure can be combined.
To represent the different states that the distributed system must encounter, weoften use predicates that include universal and existential quantifiers over the groupmembership. For example, ∀ i ∈ sites, Ki(Id(i)) defines the predicate 'each memberof the group “sites” knows its own identifier'. Ki is the knowledge predicate asdefined in [6]. Such a predicate in a state predicate must be interpreted by thefollowing informal sentence : \"In order to run correctly in this state, each object canaccess its identifier variable\".2.2. Object specifications
In our methodology, an object is an autonomous entity (as an agent) thatinteracts with the other objects of its environment using remote operations and thatowns local knowledge. For instance local knowledge of an object is the set ofvariables managed and accessed by methods of the object or synchronizationvariables such as event counters. We also deduce some local variables from globalknowledge. Using the previous example, we can say that as each object must knowits own identifier, then it must define a variable “site_identifier” to represent thisknowledge. The behavior clauses of an object define the coordination betweendifferent actions such as synchronization, scheduling of actions, and sharing ofresources. It also ensures the object coherence. When the group level specifies somegroup global state, then the object must be able to reflect itself part of this state.
2.3. Method specifications
A method specifies the internal mechanisms of the object that characterize itsbehavior when it receives a request. The local variables of a method or action can beaccessed without restriction because they are only accessed by the consideredmethod. The update of global variables of the object is restricted by the concurrencecontrol defined in the object specification. Then, the specification of the methodprovides basic algorithmic structures such as loops, tests, arithmetic operations, readsand writes of variables.
The result must be a sufficiently precise algorithmic specification associatedwith its proof in order to be easily and error free translated into a programminglanguage.
3. Semantics and syntax3.1. Definition of the components
One of the key features of our methodology is to use a common paradigm forthe three levels of specification (a state-transition approach). The same formalism isused to write models describing the behavior of a group, an object, or a method.initialstateState-predicate :Pred1
Condition : Cond;// guardAction: A;// command to performPost-condition :finalstatePredicate
State-predicate :Pred2
Fig. 3.1 : Basic components of the modelFigure 3.1 presents the basic components of a specification in a graphicalrepresentation. The model is composed of states and transitions. States are associatedwith a predicate. Transitions are edges between states and are labeled by a condition,an action, and a post-condition. The semantics of the model that is discussed in thenext sub-section supports concurrence. So the model must be clearly distinguishedfrom the sequential finite state model used in message passing protocols. Indeedseveral transitions can be fired simultaneously.
3.1.1. States
A state represents a significant point in the run of a behavior. It is characterizedby a Boolean valued predicate. A state is enabled or disabled. Each model (of thegroup, object or method level) owns a particular state that is called the initial stateand that is enabled at the creation of the group, the instanciation of the class or thebeginning of the method. It is defined to be enabled (or assessable) when reachedalong a sequence of states starting from the initial state of a behavior. Once a state isenabled its consequent transitions can be checked. Then, it is enabled as long as itspredicate is verified. Therefore several states can be enabled simultaneously, soconcurrent behaviors can be represented. If a designer wants several states to beenabled in the same time, the only constraint is that their predicates do not conflicte.g. they just have to be true simultaneously.3.1.2. Transitions
A transition delimits phases between two states in the execution of a behavior. Itis composed of three elements: a condition, an action, and a post-condition. The paircondition/action defines a guarded command [4]. Starting from an initial state, atransition allows to reach a consequent state by evaluating a condition andperforming the associated action that leads to the result specified by the post-condition. Moreover if the post-condition does not conflict with the predicate of theinitial state, then the initial state stays assessable.
The condition is a Boolean expression and acts as a guard that must beperformed. Conditions are formulas based on the traditional negation, conjunction,and disjunction connectors. They use group, object, and method variables (shared andlocal variables).
An action can be seen as a predicate transformer. It changes the initial state-predicate into the predicate of the post-condition. An action can be the invocation ofanother action using various semantics of group communication (i.e. messagepassing, remote procedure call, group procedure call, ordered multicast, causalmulticast), different operations as the read or the write of a variable, or any kind ofalgorithmic structure (i.e. tests, loops).
The post-condition is a predicate related to an action. It specifies the result ofthe executed action. This is an enhancement of an initial state-predicate by the effectof an action. When several transitions lead to the same state, the predicate of thisstate is the disjunction of post-conditions associated with each transition.3.2. Refinements
In our methodology we propose to specify a distributed algorithm by a hierarchyof models. We call refinement the process that consists in deriving a parent model toproduce a child model creating by this way a kind of inheritance hierarchy ofbehavioral models. Our basic assumption about the refinement process is that it mustreduce the space of solutions of the model (e.g. the behavior that can satisfy the
constraints specified by state predicate and transitions). To put it more precisely weassume that the set of solutions of a refined model must be a sub-set of the set ofsolutions of a parent model. The set of solutions is defined as the set of all correctimplementations (behavior compatible with the final specification).
Two situations need to be examined. We must validate a refinement betweentwo models within a same level (group, object, or method) and between two modelsof different levels.
3.2.1. Refinement within a same specification level
There are two ways of refining an action : we can split up it into several sub-actions or we can enhance the post-condition defining its results.
Let us consider an action A (Figure 3.1) that we want to refine with two or moresub-actions. In Figure 3.2a, A is refined into two sub-actions A1 and A2 that can beexecuted sequentially or concurrently. In the former situation A1 and A2 are executedsequentially. We introduce an intermediate state whose predicate is the post-condition of the first sub-action A1. In the latter situation the condition Cond isduplicated on each transition; A1 and A2 are executed concurrently. In both cases, thepredicates of the initial and of the final states (Pred1 and Pred2 respectively) areunchanged.
Pred1Condition : CondAction : A1Post : Pred12Pred12Condition : C2Action : A2Post : Pred2Pred2Pred1Condition : CondAction : A1Post : Pred21
Condition : CondAction : A2Post : Pred12Pred22Pred2 ≡Pred21 ∨
Sequential compositionParallel composition of sub-actions of sub-actions
Fig. 3.2a : Two ways of refining an action into sub-actionsThe second way of refining an action is conducted by enhancing its post-condition. Let us consider an underspecified behavior where an action is not yetdesigned. For instance, in Figure 3.2b the action modify i has no concrete algorithmicstructure. This situation is rather common when the algorithm is complex. We do notmaster all its complexity at once. Most of the time we leave parts of it underspecifiedand we assume they will be specified later. So these particular actions are onlydefined by their result (e.g. their post-condition). In Figure 3.2b the result of action
modify i is: i>0 ∧ i<10. Then a refinement step consists in defining more preciselythe post-condition: i=1. Thus, i=1 is a correct refinement of the post-condition.i = 0
Condition : trueAction : modify iPost : i > 0 ∧ i < 10i > 0 ∧ i < 10
i = 0
Condition : trueAction : modify iPost : i = 1i = 1
Fig. 3.2b : Refinement of an action by enhancing the post-condition3.2.2. Refinement between two different specification levels
Here, we consider only the refinement from a group level to an object level.This refinement depends on two distribution criteria.
First we can distribute the entities that cooperate to solve the problem accordingto the physical reality. In this situation, each agent or site has the same behavior. Wehave developed an example of a spanning tree distributed algorithm where each sitethat takes part in the construction has the same code [2]. More intuitively, when thedistributed application is symmetric (e.g. the same code runs on each site of theenvironment with different initialization parameters) then, only one model is neededto bridge the gap between the group and the object level.
The distribution of a group can be viewed with a competence approach. We splitup the problem according to the modularity principle. Each object can perform a setof different actions. Let us consider a distributed object system whose common goalis to exchange information and where an object plays the role of a data base server. Itappears that the model describing the common goal of the application needs to berefined into two distinct object level models: one for the server and one for the client.Each of these models refines a part of the global behavior of the group. We are nowtrying to find practical rules that help users to realize the transition between grouplevel and object level but there are many difficulties to give a general methodology.3.3. Proof technique
Proofs must be associated with specification models in order to assert userdefined properties. The proof technique is the same for each specification level.Starting from an initial state of one model the proof consists in establishing thatgiven the hypotheses H defined by a state-predicate, if the condition is verified andthe action is processed, then the post-condition can be deduced.
H q Condition ∧ Action ⇒ Post-Condition
4. Conclusion and Perspectives
In this paper we define a methodology that introduces guidelines useful for thespecification of distributed algorithms. Its originality is to merge concepts derivedfrom algebraic formal methods (B method), distributed artificial intelligence(knowledge operators and reflexivity), and distributed algorithms (distributed controlstructures and mechanisms for order properties). This method was used in severalsmall examples and, in particular, in the specification and proof of a spanning treedistributed algorithm [2].
There are many problems that must still be solved. From a practical point ofview, we have to improve our approach by developing several different kinds ofdistributed algorithms. From a theoretical point of view, it is important to associate ina more formal model the different modal logic tools (e.g. epistemic logic, deonticlogic, and temporal logic of actions). The behavioral reflexive approach ofdistributed artificial intelligence must be correctly integrated in our work.
Another large project is to develop a set of tools that takes into account andimplements all the previous concepts. Today our implementations are realized on theGUIDE operating system that is an interesting distributed object-oriented tool, but farfrom the previously presented concepts. Hence it does not allow to express correctlyour solutions.Bibliography
[1] J.R. Abrial. “The B-Book”, Cambridge University Press, 95, to appear, andPolycopié de cours, Valeur C, CNAM, 94.
[2] L. Bonnet, L. Duchien, G. Florin, L. Seinturier. “A Spanning Tree Object-Oriented Distributed Algorithm Specification and Proof”, Rapport de RechercheCEDRIC 95-04, January 95.
[3] C. Coste, “Appel de procédure à distance sur groupe en approche objet réparti”,mémoire CNAM, Juin 1995.
[4] E.W. Dijkstra. “A Discipline of Programming”, Prentice Hall 76.
[5] G. Florin, R. Gomez and I. Lavallee, “A distributed Recursive Solution to theshortest path problem”, Congresso IO 94, April 94, Braga, Portugal.
[6] J.Y. Halpern, Y. Moses. “Knowledge and Common Knowledge in a DistributedEnvironment”, ACM 90.
[7] C.A.R. Hoare, “The Axiomatic Basis of Computer Programming”,Communications of the ACM, 1969.
[8] L. Lamport. “The Temporal Logic of Actions”, DEC SRC R-Report 81, Dec 91.
因篇幅问题不能全部显示，请点此查看更多更全内容