Final - Volume 3 No 6

DESIGN OF FORMAL AIR TRAFFIC CONTROL SYSTEM THROUGH UML Shafeeq Ahmad Azad Institute of Engineering & Technology, INDIA [email protected] Vipin Saxena Dr. B. R. Ambedkar University, INDIA [email protected]

ABSTRACT In recent years, UML has become most popular among modeling languages and is commonly used to drive the design and implementation of system and software architectures. UML models help to achieve functional and non-functional requirements of system. Furthermore, UML tools have enabled the creation of source code from UML diagrams in order to initiate the programming phase of building software. However, due to lack of clearly defined semantics, it has been challenging to create source code from UML models. The main objective of the paper is to model Air Traffic Control system by the use of UML. An activity of Air Traffic Control i.e. departure process which only covers part of the Air Traffic Control functionality has been considered in this paper. The UML models created using formal naming semantics help them to convert into source code and also help to achieve functional and non-functional requirements. The complexity of Air Traffic Control System is also measured which makes the design simple and visibly understandable.

Keywords: UML model, formal semantics, source code, Air Traffic Control.

1

INTRODUCTION

Nowadays Object Oriented software development process is widely used in the Software Industry. The emergence of Object-Oriented programming has heavily contributed toward a standardized method of modeling known as the Unified Modeling Language (UML). In recent years, UML has become synonym for software modeling and is commonly used to model the software architecture problems. Source code can be easily be generated with the help of different UML diagrams for building the software. To generate the correct source code, the main problem is lack of clearly defined semantics and code generation can only be done if the UML specification is standard, complete, precise, and unambiguous. The present work is based upon the ATC system which is explained below: 1.1 ATC System ATC system is a service that gives guidance to aircraft, prevents collisions and manages safe & orderly traffic flow. It is a vast network of people & equipment that ensures safe operation of aircrafts.

UbiCC Journal - Volume 3

The first air traffic control (ATC) system was originally built in the 1960s; since then, air traffic has increased immensely, and has become increasingly more difficult to maintain safety in the sky. As air travel has become an essential part of modern life, the ATC system has become strained and overworked. The ATC system has been in a process of continuous improvement / change. In the earliest days of aviation, few aircraft were in the skies that there was little need for automated control of aircraft. As the volume of air traffic increased and the control was still fully manual; the system was considered unsafe as human error has been cited as a major factor in the majority of aviation accidents and incidents. In today’s Air Traffic Control system, air traffic controllers are primarily responsible for maintaining aircraft separation. Every aircraft follows several activities during a flight. These activities are shown below in Fig.1: (i) Preflight -This portion of the flight starts on the ground and includes flight checks, push-back from the gate and taxi to the runway.

Page 1

(ii) Takeoff - The pilot powers up the aircraft and speeds down the runway. (iii) Departure - The plane lifts off the ground and climbs to a cruising altitude. (iv) En route - The aircraft travels through one or more center airspaces and nears the destination airport. (v) Descent - The pilot descends and maneuvers the aircraft to the destination airport. (vi) Approach - The pilot aligns the aircraft with the designated landing runway. (vii) Landing - The aircraft lands on the designated runway, taxis to the destination gate and parks at the terminal. En Route Departure Preflight

Takeoff

Descent Approach Landing

(iii) Outdated design/technology – Obsolete software design and programming language [11] are major barriers to upgrades and efficient software maintenance of the currently used ATC systems because of which improved capacity and efficiency can’t be achieved with the current system. The current computer software limits the number of aircraft that can be tracked at any given time, and the dated architecture makes enhancements, troubleshooting and maintenance more difficult. Computer outages, planned or unplanned, are covered by a backup system that cannot handle the same level of air traffic as the main system. The result is significantly limited capacity during backup mode. (iv) Mixed communication – The communication between the controllers & pilot currently is a combination of voice & datalink. The results of test conducted [18] show that the mixed communication leads to slow speed which can be overcome only when the whole communication takes place in a well defined manner . 2

Figure 1: Activities of Aircraft [6] 1.2 Drawbacks of Current ATC System ATC systems are highly complex pieces of machinery, they employ standard verification and modeling technique to coordinate, distribute and track aircraft as well as weather information. The currently used systems need to employ procedures for improved safety and efficiency which include flexibility, potential cost savings & reduction in staffing. This means that there is a lack of advanced technology and desire to support the controller. Thus there is a need to build ATC system based on a method which can handle increased air traffic capacity/congestion to provide a safety critical interactive system. The following are the major drawbacks of current ATC system: (i) Lack of well-defined human/software interface – The idea of full automation or minimum human intervention of the ATC system still remains unfulfilled. The existing systems do require human interaction as the system only guides but actual decision is taken by the controllers incharge (ground, local). (ii) Need for high maintenance – Maintenance of the system is also an issue which can cause problem as discussed by Matthew L. Wald [23] about an incidence in which voice communication between the pilot & controllers broke down & the reason behind this was found to be a lack of maintenance.

UbiCC Journal - Volume 3

RELATED WORK

The ATC system consists of controllers & technology. The various controllers involved have different tasks assigned to them which have been very well described in [15], [16], [19], [20]. The ATC real-time system [19] is characterized as complex, time-driven and potentially distributed. It is composed from multiple sub-systems, which must cooperate in order to complete its real time targets. ATC employs the approach of Parallel Applications in which the simultaneous execution of some combination of multiple instances of programmed instructions and data on multiple processors are performed in order to obtain results faster. Meilander [4] has proposed a solution for problems arising due to parallel processing used in ATC but its implementation needs reliable software. The reason for system failure discussed in [8] was found to be lack of maintenance. For the efficient software maintenance, [11] emphasizes changes particularly on the technology front which means modernizing the current air traffic control system by replacing the software used in the current ATC systems. The study done by Verma[18] by implementing changes in the procedures, roles and responsibilities of the controllers for redistribution of workload and communications among them, has also stressed on the introduction of new automated technologies for the controllers. For a critical system like ATC an extremely low probability of failure is needed as if the system fails any related type of hazard can occur. The reports on incidences at non-controlled airports [5] show that

Page 2

pilots can’t entirely rely on vision to avoid collision & also it is necessary to get all the air-traffic related information correctly. So it is crucial that in such large and extremely complex systems the software is designed with a sound architecture A good architecture not only simplifies construction of the initial system, but even more importantly, readily accommodates changes forced by a steady stream of new requirements. This architectural construct can be derived from modeling concepts by using the powerful extensibility mechanisms of UML [1]. The UML model-based approach helps to manage critical systems, since the model support the necessary analysis activities in several ways: • The formalized structural and behavioral system description gives the necessary basis for criticality analysis. • Providing behavior is expressed in simple state charts or “English-like” pseudo code, the behavior should at least be explainable to endusers. • The model gives an excellent basis for faulttolerance analysis, since the model includes the dependency structure. The size and complexity of the ATC system demand a considerable initial development effort, typically involving large development teams, that is followed by an extended period of evolutionary growth. During this time new requirements are identified and the system is modified incrementally to meet them. Under such circumstances an overriding concern is the architecture of the software. This refers to the essential structural and behavioral framework [1] on which all other aspects of the system depend. Any change to this foundation necessitates complex and costly changes to substantial parts of the system. Therefore, a welldesigned architecture is not only one that simplifies construction of the initial system, but more importantly, one that easily accommodates changes forced by new system requirements. To facilitate the design of good architecture the domain-specific usage can be implemented using the UML. Object-oriented requirements analysis using modular and decomposable use cases provide to be very powerful method for the analysis of large-scale ATC systems [6]. It is extremely useful to define both the static semantics (i.e., the rules for wellformedness) and the dynamic (run-time) semantics of the ATC system. These semantic rules fully defined and consistent, and in conjunction with an action specification language that is also complete and consistent can be used to specify the details of state-transition (Activity diagram of UML) actions, Interaction (Sequence diagram of UML) and object methods (class diagram of UML) and the resulting models will be executable. Furthermore, if all the

UbiCC Journal - Volume 3

necessary detail is included in a model, such model can be used to automatically generate complete implementations. The role of software architecture is similar in nature to the role architecture plays in building construction. Building architects look at the building from various viewpoints useful for civil engineers, electricians, plumbers, carpenters and so on. This allows the architects to see a complete picture before construction begins. Similarly, architecture of a software system is described as different viewpoints of the system being built. These viewpoints are captured in different model views. UML provides a number of diagram types for creating models. UML does not specify what diagrams should be created or what they should contain, only what they can contain and the rules for connecting the elements. Some UML diagrams can have different uses and interpretations. The result of this has been that behavioral and/or run-time semantics are not well defined for standard UML modeling elements. The semantics problems have made it difficult to achieve model-based programming using standard UML. Hence semantically correct UML models [12], [17] are needed to achieve code. Also the UML models enhance communication as they provide a better way to understand and communicate among analysts, designers, developers, testers and with domain experts for designing a system. Creating and debugging software code has been and continues to be a very labor-intensive and expensive process but having an accurate UML model can ease the work as if any problem comes and modification is required then instead of modifying the code the models can be modified, even the extensibility can be done by adding new constructs to address new development issue. To meet the non-functional requirements [13] such as modifiability, testability and reliability, the design and analysis of a system at the architecture design level must be done. Non-functional requirements have a critical role in the development of a software system as they can be used as selection criteria to help designers with rational decision-making among competing designs, which in turn affects a system’s implementation .Thus the ATC system needs to provide a sufficient amount of dependability and should support a survivability architecture [10]. In this paper we examine the most important modeling constructs used for representing the ATC system handling departure and also describe how they are captured and rendered using UML. The models are based on the work presented by Saxena & Ansari [21].The operations, phases and controllers involved during departure of an aircraft have been described in [2], [3], [7], [9], [10], [14], [15], [19] &

Page 3

[20] which have been used as base for designing various UML models. 3

PROPOSED APPROACHED

The existing systems are quite complex and inefficient. To adapt to the changing demands of speed and efficiency a reliable software system for ATC is required to be developed. Software architecture based on UML models will help in handling complexities and drawbacks of existing ATC systems and also help to better understand the domain. UML is the de-facto standard visual modeling language which is a general purpose, broadly-applicable tool supported, industrystandardized modeling language which offers an extensive set of diagrams for modeling. The complexity of the problem domain requires extensive efforts for the clarification of the initial problem statement. Moreover, due to the extremely long lifespan of ATC systems, stable and robust analysis models enabling the integration of new operational scenarios are needed which can be efficiently obtained using UML models. In the design of a departure activity of ATC system UML will help to meet safety, reliability, availability, and robustness demands in an environment of steadily increasing air traffic density. The code obtained using the UML models is highly optimized which is one of the main requirements for the design of a cooperative ATC system. 4

DESIGN OF ARCHITECTURE

System architecture is a set of design decisions. These decisions are technical and commercial in nature. To meet the functional and nonfunctional requirements of the above said ATC system it is necessary to model the complete ATC system by the use of UML. Different types of diagrams are designed and described below in brief: 4.1 UML Activity Diagram Activity diagram describes the workflow behavior of a system. It illustrates the dynamic nature of a system by modeling the flow of control from activity to activity. An activity represents an operation of a class, resulting in system state change.

UbiCC Journal - Volume 3

The informal activity diagram for departure of an aircraft is given below in Fig. 2. It simply describes the main activities performed during departure by the controller and the aircraft object. In this diagram some semantic problems are present like if any clearance has not been granted then what will be done is not clear i.e. use of decision box hasn’t been done. Further all the activities have been shown in a single step and no refinements have been done to simplify the activities. These loose semantics of the diagram make this model unable to be executable, therefore the formal activity diagram for departure of an aircraft is defined and shown in Fig. 3 Aircraft

Controller

Request pushback clearance Grant pushback clearance

Pushback from gate

Leave ramp area

Request taxi clearance Grant taxi clearance

Taxiing

Request departure clearance

Grant departure clearance

Depart

Figure 2: Informal UML activity diagram of departure activity of a flight

Formal activity diagram [fig.3] contains five objects aircraft, Gate_controller, Local_ controller, Ramp_controller & Ground_controller. It describes various activities which are performed by all the objects. While these activities/operations are being done, it also shows in which state the system is like ready for departure, taxiing etc. There is a request by the pilot of the aircraft to the gate controller to assign

Page 4

Figure 3: Formal UML activity diagram of departure activity of a flight

UbiCC Journal - Volume 3

Page 5

it a gate which is the initial state & the final state is named as depart. When the next activity is performed the system is taken to the next state that means a transition causes the change of state. Against the transitions various conditions are listed which actually cause the transition. Also the use of decision box is applied which is required to check whether the various clearances like pushback, taxiing & final departure clearance has been granted or not. If clearance has been granted then only the aircraft starts pushing back or departing else if because of some reason clearance could not be granted then it will again go to the request clearance state where it will be seen & tracked until it is safe for pushback or departure. During the whole departure activity the possibilities of any emergency condition is also taken into consideration and shown in the diagram. Hence the solid and well organized semantics like conditions for transitions, use of swimlanes, fork, join, method calls from objects i.e. able to call methods from other objects, decision condition specification etc. have been used in this diagram which make this model executable.

it lacks concrete, well defined semantics which make it impossible to help it in bringing to a computational consistency, therefore formal use case diagram is drawn for departure activity of a flight and shown below in Fig. 5.

Ramp_controller

Govern ramp area

Gate_controller gate freeing

clearance to leave ramp

assign gate

<<extend>>

Taxiing

grant pushback from gate

sequencing at ramp

<<extend>>

Monitoring Taxiing

Grant Clearances

Pushback

Controller

Tracking & Maintaining safe distance

Aircraft

Departure

Handle aircraft movement

Provide information

Aircraft sequencing

Figure 4: Informal UML use case diagram of departure activity of a flight

This diagram consists of two actors namely controller and aircraft. The use-cases consists represent the functionality of both actors. But this use case diagram provides an informal viewpoint as

UbiCC Journal - Volume 3

clearance for taxiing

<>

pushback

<<extend>>

Handle surface movement

Tracking

<>

Taxi-plan

<>

Detect actual runway exit

Departure queue sequencing

Aircraft <<extend>>

select for departure clearance for takeoff

Local_controller

<>

<<extend>>

Maintaining safe distance between planes <>

<>

4.2 UML Use Case Diagram The use case diagram captures system functionality as seen by users. It shows an outside-in view of the procedures available in the use of the system i.e. all the available functionality of the system is represented at a high level. The UML models can package the most relevant activities in use cases and identify important actors. The UML use case diagram for departure activity of ATC system is shown in Fig.4.

Ground_controller

<> <>

enter and leave ramp

Sectorization

Information of weather, speed and direction

Sequencing at holding points

departure

Departure Departure <>

Monitor runway incursions

Figure 5: Formal UML use case diagram of departure activity of a flight In the above model there are all five actors namely Aircraft, Ground_controller, Ramp_controller, Gate_controller & Local_ controller which interact with various use cases. The use cases clearly describe various main functions during departure and whether they are dependent on each other directly or indirectly denoted by extended or included keywords. It explains actually which functions are governed by which actors. This diagram provides the functional basis for creating the remainder of the diagrams needed to arrive at an executable diagram as it has well defined semantics like identifying every actor involved during departure of a flight, specifying all the functions performed by each actor and use of extend or include keyword to identify how one function of an actor is related to another. This formal use case diagram also drives the design of the class diagram, and sequence diagram. 4.3 UML Class Diagram Class diagram identifies & describes the static structure of the system i.e. the system architecture.

Page 6

The following Fig.6 shows the informal class diagram of the departure activity of a flight. Controller controllername location area

Aircraft aircraftname airlinename departuretime

monitor() grantclearance() tracking() movementhandling()

pushback() taxi() depart()

Figure 6: Informal UML class diagram of departure activity of a flight This diagram gives a general view of the classes involved during departure namely the controller and the aircraft class. In this diagram only the name of the attributes and the operations of the classes have been specified. Even the attribute type or the return type of the methods hasn't been described. These loose semantics make this model impossible to compile and execute. Now let us examine a formal class diagram of departure activity of a flight shown below in Fig.7

some distinct attributes (properties) and some operations which are listed in the 2nd and 3rd section respectively of the class diagram. The type of attributes and return type of operations have been clearly specified in the diagram. This class diagram has covered almost all the explicitly defined semantics like class relationships, multiplicities, associations, properly labeled relationships, strict naming of classes, attributes, and methods, explicit parameters/return values which are necessary in order to allow the model to be computationally executable. 4.4 Sequence Diagram A sequence diagram is an interaction diagram that details how operations are carried out, what messages are sent and when. Sequence diagrams have a temporal focus so they are organized according to time which means what happens when. The informal sequence diagram of departure activity of a flight is shown below in Fig 8. It simply gives a sequence of messages between the controller

Gate_controller gatename : Variant gateassignment() makegateavailable() pushbackclearance() : Boolean +gate clearance granting 1

controls 0..* Aircraft airlinename : String aircraftnumber : Variant airplanetype : String position : Variant altitude : Integer departuretime : Date departureairport : String speed : Integer distance : Integer route : Variant callsign : String trajeventlist : Variant latitude : Integer longitude : Integer +assigned aircraft

Ground_controller location : Variant area : Integer inactiverunwayname : String monitoringdevice : String holdingareas() +taxi clearance granting controlgroundtraffic() 1 controls protectcriticalareas() 0..* departurequeuesequencing() +assigned aircraft handleemergencies() taxiclearance() : Boolean +assigned aircraft

0..*

controls 1

depart() taxiing(taxi-out-plan, assigned-runway) pushback() getdeparturetime() assignflightcreww() maneuvering() delayflight(number of minutes) setcallsign(string callsign value) getcallsign(string callsignvalue) addtrajevent()

+ramp clearance granting

Ramp_controller ramparea : Long controlrampoperations() sequencingatramp() aircraftservicing() aircraftloading() rampclearance() : Boolean

Local_controller sector : String location : Variant activerunwayname : String radarcoverage : Long +assigned aircraft

0..*

controls 1

+departure clearance granting

givinginformation() : Variant clearance() selectfromqueue() handleemergencies() sectorization() runwayassignment() monitorrunwayincursions() holdingpointsequencing() consists of

1 Clearance_delivery_controller aircraft : String clearancelimit : Long departurefrequency : Integer routeassigned : Variant altitudeassigned : Double routechecking() finaldepartureclearance() : Boolean

Figure 7: Formal UML class diagram of departure activity of a flight This class diagram of the departure activity of a flight described in Fig. 7 focuses on the main objects and associations (relation) between them. During departure main objects are Gate_controller, Ramp_controller, Ground_controller, Local_controller and Aircraft itself. The Local_controller in turn consists of the Clearance_delivery_controller which gives the final departure clearance. Also a controller called Ramp_controller is present which is just a type of ground controller which is responsible for operations at ramp (parking) area. All the objects in turn have

UbiCC Journal - Volume 3

Figure 8: Informal UML sequence diagram of departure activity of a flight

and the aircraft objects. But this model doesn’t include the semantics necessary for making it executable as no parameter values are specified, no guards have been used for any decision point, even the class definition is not necessarily present in the called class. Hence this model can not be compiled and executed, therefore a formal sequence diagram is defined & shown in Fig.9.

Page 7

Figure 9: Formal UML sequence diagram of departure activity of a flight

UbiCC Journal - Volume 3

Page 8

In Fig.9 complete departure activity of a flight can be seen at a glance. The messages are communicated between the five main objects; aircraft, Gate_controller, Ramp_controller, Local_controller and Ground_controller. It clearly describes the interaction between the objects and gives the order or sequence in which the actions take place i.e. in what order messages have been send. The solid lines represent the call messages while the dotted lines represent the messages returned between the objects. The tags are added to clearly specify about the operation. This model consists of all the clear semantics like use of tags, explicit parameter values, explicit return values, combined fragments(alternatives and parallel), guards needed for decision points and all the class definitions exist in the called class. Thus this formal sequence diagram with well defined and solid semantics makes it able to be compiled and computationally executable. 5

[5]

[6]

[7]

[8]

[9]

CONCLUDING REMARKS [10]

From the above work it is concluded that the described software architecture design process fully covers the departure activity of an aircraft. UML modeling has been used for making the various models (class, use-case, activity & sequence) using informal and formal semantics. These designed models are essential part of architecture of ATC software system and that can help to achieve executable code and other functional and nonfunctional requirements of software system. 6 [1]

[2]

[3]

[4]

REFERENCES B. Selic, and J. Rumbaugh, “Using UML for Modeling Complex Real-Time Systems”, March 1998. Available: http://www.ibm.com/ developerworks/rational/library/content/03July/ 1000/1155/1155_umlmodeling.pdf I. Anagnostakis, H. R. Idris, J. P. Clarke, E. Feron, R. J. Hansman, A. R. Odoni, and W. D. Hall, "A Conceptual Design of A Departure Planner Decision Aid", 3rd USA/Europe Air Traffic Management R & D Seminar, June 1316, 2000. Available: http://dspace.mit.edu/ bitstream/1721.1/37321/1/paper68.pdf, H. Idris, J. P. Clarke, R. Bhuva, and L. Kang, “Queuing Model for Taxi-Out Time Estimation”, Sep 2001. Available: http://dspace.mit.edu/ bitstream/1721.1/37322/1/TaxiOutModel.pdf W. C. Meilander, M. Jin, and J. W. Baker, “Tractable Real-time Air Traffic Control Automation”, International Conference on Parallel and Distributed Computing Systems, pp. 477-483, November 4-6, 2002.

UbiCC Journal - Volume 3

[11]

[12]

[13]

[14]

[15]

[16]

[17]

G. Brown, “Remote Intelligent Air Traffic Control Systems for Non-controlled Airports”, Jan. 2003. Available: ww4.gu.edu.au:8080/adtroot/uploads/approved/adtQGU20040225.084516/ public/02Whole.pdf, J. Whittle, J. Saboo, and R. Kwan, “From Scenarios to Code: An Air Traffic Control Case Study”, 25th International Conference on Software Engineering (ICSE'03), pp. 490, 2003 Safety Regulation Group, “Air Traffic Services Information Notice”, ATS Standards Department, Civil Aviation Authority, no. 50, Aug. 2004. M. L. Wald, “Maintenance Lapse Blamed for Air Traffic Control Problem” The New York Times, Sep 2004. Available: http://www.nytimes.com/2004/09/16/politics/16 airports.html M. Axholt, and S. Peterson, “Modelling Traffic scenarios for Realistic Air Traffic Control Environment Testing”, Linkoping University Press, Department of Science & Technology, Linkoping University Sweden, Nov. 2004. R. D. Lemos, C. Gacek, and A. Romanovsky, “Architecting Dependable Systems II”, Springer-Verlag Berlin Heidelberg, 2004. ATCA Air traffic Control Association, “Air Traffic Control Computer Modernization is En Route”, Feb 2005. Available: http://www.atca.org/news.asp Object management Group, "Unified Modeling Language: Superstructure", Version 2.0, Formal/05-07-04, Aug 2005, Available: http://www.omg.org/docs/formal/05-07-04.pdf L. Dai, and K. Cooper, “Modeling and Analysis of Non-functional Requirements as Aspects in a UML Based Architecture Design”, Proceedings of the Sixth International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing and First ACIS International Workshop on SelfAssembling Wireless Networks (SNPD/SAWN’05) , IEEE 2005. European Organisation For The Safety Of Air Navigation (Eurocontrol), “WP 5.2 – Add NFR To Use Cases And Interaction diagrams NFR Mapping Report”, June 2006. P. A. Bonnefoy, "Airport Operations ", MIT, Air Traffic Control, MIT International Center for Air Transportation, Sep 2006 R.J. Hansman, “Air Traffic Control Overview”, MIT Department of Aeronautics and Astronautics, MIT ICAT, Available: http://ocw.mit.edu/NR/rdonlyres/Aeronauticsand-Astronautics/16-72Fall-2006/11CD67DE29C1-4AB9-A7DD-004BB1897CB9/0/ lec1.pdf R. Campos," Model Based Programming: Executable UML With Sequence Diagrams ", A Thesis Presented to The Faculty of the Computer

Page 9

[18]

[19]

Science Department, California State University, Los Angeles, June 2007 S. Verma, T. Kozon, V. Cheng, and D. Ballinger, “Changes In Roles/Responsibilities of Air Traffic Control Under Precision Taxiing”, 26th IEEE/AIAA Digital Avionics Systems Conference, Oct 2007 Wikipedia, “Air traffic control”, October 2007. Available: http://en.wikipedia.org/wiki/Air_traffic_control

UbiCC Journal - Volume 3

[20]

[21]

L. Brim, “ Fundamentals of Air Traffic Control”, ParaDise Seminar, Feb 2008, Available: http://www.fi.muni.cz/paradise/Seminar/2008spring/0225-prezentace.pdf V.Saxena, and G.A.Ansari, ”UML Models of Aircraft System”, ICFAI Journal of Systems management, Vol. 6, No.2, PP. 68-74, May 2008

Page 10

LRN/R-MAUDE BASED APPROACH FOR MODELING AND SIMULATION OF MOBILE CODE SYSTEMS Laïd Kahloul1 and Allaoua Chaoui2 Computer Science Department, Biskra University, Algeria [email protected] 2 Computer Science Department, Constantine University, Algeria [email protected] 1

ABSTRACT Code mobility technologies attract more and more developers and consumers. Numerous domains are concerned, many platforms are developed and interest applications are realized. However, developing good software products requires modeling, analyzing and proving steps. The choice of models and modeling languages is so critical on these steps. Formal tools are powerful in analyzing and proving steps. However, poorness of classical modeling language to model mobility requires proposition of new models. The objective of this paper is to provide a formal approach based on LRN and R-Maude. LRN (Labeled Reconfigurable Nets) is a specific formalism that we propose to model different kinds of code mobility. R-Maude (Reconfigurable Maude) is a system that we devlop to encode and simulate LRN-models. Keywords: code mobility, modeling mobility, LRN, R-Maude. found in process algebra based model and state transition model. For the first one, π-calculus [13] 1 INTRODUCTION is the famous one, and for the second, high-level Petri net (with many kinds) can be considered the Code mobility is one of the attracting fields for good representative. π-calculus is an extension for computer science researchers. Code mobility CCS (communicating concurrent systems) [12]. technology seems an interest solution for CCS allows modeling a system composed of a set distributed applications facing bandwidth problems, of communicating process. This communication users' mobility, and fault tolerance requirement. uses names (gates) to insure synchronization Numerous platforms were been developed [17]. between processes. In π-calculus information can Such platforms allow the broadcasting of this been exchanged through gates. The key idea is that technology in many domains (information this information can be also a gate. With this idea, retrieving [9], e-commerce [11], network process can exchange gates. Once these gates management [22], …). Software engineering received, they can be used by the receiver to researches have provided some interest design communicate. In an extension of π-calculus, HOπparadigms influencing the development of the field. calculus [15], processes can exchange other The most recognized paradigms [7] are: code on processes through gates (the exchanged processes demand, remote evaluation, and mobile agent. To called agents). avoid ad-hoc development for code mobility To model mobility with Petri nets, high level software, many works attempt to propose PNets were proposed. The most famous are Mobile methodologies and approaches ([16], [21], [14], Nets (variant of coloured Petri nets) [1] and …). Indeed, these approaches are mostly informal. Dynamic Petri nets. In mobile Petri nets, names of They lack in analyzing and proving system places can appear as tokens inside other places. proprieties. Enhancing development process with Dynamic Petri nets extend mobile Petri nets. In this formal tools was an attractive field in code mobility last one, firing a transition can cause the creation of researches. a new subnet. With high-level Petri nets, mobility Traditional formal tools witch were massively in a system is modeled through the dynamic used to model and analyze classical systems seem structure of the net. A process appearing in a new to be poor to deal with inherent proprieties in code environment is modeled through a new subnet mobility systems. Works on formal tools attempt to created in the former net by firing a transition. extended classical tools to deal with code mobility Many extensions have been proposed to adapt proprieties. The most important proposition can be mobile Petri net to specific mobile systems: Elementary Object Nets [18], reconfigurable nets [3], Nested Petri Nets [10], HyperPetriNets [2], … With respect to [20], all these formalisms lack in

UbiCC Journal - Volume 3

Page 11

security aspect specification. To handle this aspect in code mobility, recently Mobile Synchronous Petri Net (based on labeled coloured Petri net) are proposed [19]. The objective of this work is to treat to aspects of code mobility: modeling and simulation. We try to propose a formal approach in witch we define two formalisms : Labeled Reconfigurable Nets (LRN) and Reconfigurable Maude (R-Maude). Firstly, LRN will be used to model the system then R-Maude will encode and simulate this model. Our formalism “labeled reconfigurable nets” with a different semantic from the one presented in [3] is dedicated to model code mobility systems. We attempt to propose to model mobility in an intuitive and an explicit way. Mobility of code (a process or an agent) will be directly modeled through reconfiguration of the net. We allow adding and deleting of places, arcs, and transitions at run time. R-Maude is an extension for Maude that we propose and prototype in order to encode and simulate LRN models. The rest of this paper is organized as follows. Section 2 starts by presenting the definition of the formalism LRN. In section 3 we show how LRN can be used to model the three mobile code paradigms: “remote evaluation”, “code on demand”, and “mobile agent”. Section 4 presents the idea and foundation of R-Maude, and section 5 discusses the prototype and shows an example. In section 6, we present some related works. We conclude this work and give some perspectives, in section 7. 2

LABELED RECONFIGURABLE NETS

Labeled reconfigurable nets are an extension of Petri nets. Informally, a labeled reconfigurable net is a set of environments (blocs of units). Connections between these environments and their contents can be modified during runtime. A unit is a specific Petri net. A unit can contain three kinds of transitions (a unique start transition: , a set of ordinary transitions: , and a set of reconfigure transitions: ). Preconditions and post-conditions to fire a start or an ordinary transition are the same that in Petri nets. Reconfigure transitions are labeled with labels that influence their firing. When a reconfigure transition is fired, a net N will be (re)moved from an environment E towards another environment E’. The net N, the environment E and E’ are defined in the label associated to the transition. After firing a reconfigure transition, the structure of the labeled reconfigurable net will be updated (i.e some places, arcs, and transitions will be deleted or added). Here after we give our formal definitions of the concepts: unit, environment and labeled reconfigurable net. After the definition, we present the dynamic aspect of this model.

UbiCC Journal - Volume 3

Formal Definition: Let N1, N2, … Nk be a set of nets. for each i: 1, …, n : Ni = (Pi, Ti, Ai), such that : 1. Pi = {pi1, pi2, …, pin} a finite set of places, 2. Ti = STi∪RTi • STi={sti1, sti2, …, stim} a finite set of standard (ordinary) transitions, • RTi = {rti1, rti2, …, rtir} a finite set (eventually empty) of “reconfigure transitions”, 3. Ai ⊆ Pi x Ti ∪ Ti x Pi. Definition 1 (Unit): a unit UN is a net Ni that has a specific transition stij denoted starti. So Ti={starti}∪STi∪RTi. Définition 2 (Environment): an environment E is a quadruplet E=(GP, RP, U, A) • GP = {gp1, gp2, …, gps} a finite set of specific places : “guest places ”; • RP = {rp1, rp2, …, rps} a finite set of specific places : “resource places”; • U = { N1, N2, … Nk} a set of nets. • A⊆ GP x StrT∪RPxT. Such that : StrT={start1, start2, …, startk} and T=ST1∪RT1 ∪ ST2∪RT2∪ … ∪ STk∪RTk Definition 3 (Labeled reconfigurable net): A labeled reconfigurable net LRN is a set of environments. LRN={E1, E2, …, Ep} such that • There exist at least one net Ni in LRN such that RTi ≠ ∅; • For each rtij ∈ RTi, rtij has a label , such that N is a unit, Ee and Eg are environments, ψ a set of places, β a set of arcs. Dynamic of labeled reconfigurable nets: Let LRN = {E1, E2, …, Ep} be a labeled reconfigurable net, Let Ei = (GPi, RPi, Ui, Ai) be an environment in LRN, • GPi = {gp1i, gp2i, …, gpsi}; • RPi = {rp1i, rp2i, …, rppi} ; • Ui = { N1i, N2i, … Nki}; • Ai ⊆ GPi x startsi ∪ RPi x Ti ∪ Ti x RPi, where: Sartsi = {start1, start2, ..., startk} and i T ={STi1, STi2, ..., STik}∪{RTi1, RTi2, ..., RTik} Let RTji be the non empty set of reconfigure transitions associated with the net Nji. RTji={rtj1, rtj2, …, rtjr}. Let rtjm < N, Ee, Eg, ψ, β> be a reconfigure transition in RTji, such that : • Ee=(GPe, RPe, Ue, Ae); • N=(P, T, A) and N∈Ue; • Eg=(GPg, RPg, Ug, Ag);

Page 12

• ψ ⊆ RPe; ψ=ψr ∪ψc. (ψr denotes removed places and ψc denotes cloned places). • β is a set of arcs. β ⊆RPe x T∪RPg x T. Let strt be the start transition of N. Conditions to fire rtjm: In addition to the known conditions, we impose that there exists a free place pg in GPg; witch means: for each t∈ startsg, (pg,t)∉Ag. j

After firing rt m: In addition to the known post-condition of a transition firing, we add the following postcondition: LRN will be structurally changed such that: If Ee and Eg denote the same environment then LRN will be not changed; Else: 1) Ug Å Ug∪{N}; Ue Å Ue/{N}; 2) Ag Å Ag∪(pg, strt); 3) Let DA ={(a, b)∈ Ae/ (a∉ψ and b∉ψ) and ((a∈N and b∉N) or (a∉N and b∈N))}, Ae=AeDA. DA –deleted arcs- to be deleted after moving N. 4) RPg Å RPg∪ψ; RPeÅRPe/ψr 5) if ALRN is the set of arcs in LRN, ALRNÅALRN∪β . 3

MODELING MOBILITY PARADIGMS WITH LABELED RECONFIGURABLE NETS

A mobile code system is composed of execution units (EUs), resources, and computational environments (CEs). EUs will be modeled as units and computational environments as environments. Modeling resources requires using a set of places. Reconfigure transitions model mobility actions. The key in modeling mobility is to identify the label associated with the reconfigure transition. We must identify the unit to be moved, the target computational environment and the types of binding to resources and their locations. This label depends on the kind of mobility. In general, a reconfigure transition rt is always labeled <EU, CE, CE’, ψ, β>, such that: • EU: the execution unit to be moved. • CE, CE’: respectively, resource and target computational environments. • ψ: will be used to model transferable resources. So ψ is empty if the system has no transferable resource. • β: models bindings after moving. The execution unit that contains rt and the EU that represents the first argument in the label will be defined according to the three design paradigms: remote evaluation (REV), code on demand (COD), and mobile agent (MA).

UbiCC Journal - Volume 3

3.1. Remote Evaluation In remote evaluation paradigm, an execution unit EU1 sends another execution unit EU2 from a computational environment CE1 to another one CE2. The reconfigure transition rt is contained in the unit modeling EU1, and EU2 will be the first argument in rt’s label. Example 4.1: Let us consider two computational environments E1 and E2. Firstly, E1 contains two execution units EU1 and EU2; E2 contains an execution unit EU3. The three execution units execute infinite loops. EU1 executes actions {a11, a12}, EU2 executes actions {a21, a22, a23}, and EU3 executes actions {a31, a32}. a21 requires a transferable resource TR1 and a non-transferable resource bound by type PNR1 witch is shared with a11. a22 and a12 share a transferable resource bound by value VTR1, and a23 requires a non-transferable resource NR1. In E2, EU1 requires a nontransferable resource bound by type PNR2 to execute a31. PNR2 has the same type of PNR1. The system will be modeled as a labeled reconfigurable net LRN. LRN contains two environments E1, E2 that model the two computational environments (CE1 and CE2). Units EU1 and EU2 will model execution units EU1 and EU2, respectively. In this case, the unit EU1 will contain a reconfigure transition rt<EU2,E1,E2,ψ,β>; such that: 1. E1 =(RP1, GP1, U1, A1); RP1= {TR1, PNR1, VTR1, NR1}. U1 = {EU1, EU2}; 2. E2 = (RP2, GP2, U2, A2); RP2={ PNR2}. GP2 ={PEU1}. 3. ψr={TR1}, ψc={VTR1}; 4. β={(PEU1,str2), (PNR2,a21), (NR1, a23)}. Fig. 1 shows the configuration before firing rt, and Fig. 2 shows the configuration after the firing.

Page 13

PEU1

E1

E2

PEU1

PEU2

str1

PEU1 PEU2

P11

str2

TR1

str3

PNR2 P21 a21

str3 P21

P12

a21 a31

PNR2

P22

a12 NR1

PNR1 TR1

VTR1

P22

P32

a22 a12

E2 PEU2

P21

rt<EU2, E2, E1, ψ, β>

P22

P13

str1

P31

a31

VTR1

PEU2

P11

PNR1 a11

PEU1

str2

rt<EU2, E1, E2, ψ, β> P12

E1

a22

a32

a32

P23

P23

P23

NR1

a23

a23

a33

Figure 1: REV-model before firing rt Figure 3: COD-model before firing rt E1

PEU1 PEU2

E2

PEU1

PEU1 PEU2

str1 str2 P11

PNR2

P21 rt<EU2, E1, E2, ψ, β>

a11

TR1

P22

PNR1 VTR1

a31 VTR1

a22

P13 NR1

P23

E1

str1

PEU1

PEU2

PNR1

E2

str3

str2

P11

P31 P31

a21

P12

str3

PEU2

P32 a32

a11 P12

rt<EU2, E2, E1, ψ, β>

TR1 a31

PNR2

a21 P23

a12

VTR1

VTR1

a32

a22 NR1

a12 a23

Figure 2: REV-model after firing rt

P32

P33

P24 a33 a23

3.2. Code On Demand In code-on-demand paradigm, an execution unit EU1 fetches another execution unit EU2. The reconfigure transition rt is contained in the unit modeling EU1, and EU2 will be the first argument in rt’s label. If we reconsider the above example, the unit EU1 will contain a reconfigure transition rt<EU2, E2, E1, ψ, β>. Fig. 3 and Fig. 4 shows the model proposed for this system.

Figure 4: COD-model after firing rt

The transition rt<EU2, E2, E1, ψ, β> means that EU1 will demand EU2 to be moved from E2 to E1. In this case, ψ={TR1, VTR1}, β={(PEU2, str2), (PNR2, a21), (NR1, a23)}. Fig.3 shows the configuration before firing rt, and Fig.4 shows the configuration after the firing.

3.3. Mobile Agent In mobile agent paradigm, execution units are autonomous agents. The agent itself triggers mobility. In this case, rt –the reconfigure transition- is contained in the unit modeling the agent and EU (the first argument) is also this agent.

UbiCC Journal - Volume 3

Page 14

Example 4.2: let E1 and E2 two computational environments. E1 contains two agents, a mobile agent MA and a static agent SA1; E2 contains a unique static agent SA2. The three agents execute infinite loops. MA executes actions {a11, a12, a13 }, SA1 executes actions {a21, a22, a23}, and SA2 executes actions {a33, a32}. To be executed, a11 require a transferable resource TR1 and a nontransferable resource bound by type PNR1 witch is shared with a21. a12 and a22 share a transferable resource bound by value, and a13 and a23 share a non-transferable resource NR1. In E2, SA2 requires a non-transferable resource bound by type PNR2 to execute a32. PNR2 has the same type of PNR1. The system will be modeled as a labeled reconfigurable net LRN. LRN contains two environments E1 and E2 that model the two computational environments. In this case the unit A that models the mobile agent A will contain a reconfigure transition rt < A, E1, E2, ψ, β >; such that: 1. E1 =(RP1, GP1, U1, A1); RP1 contains at least four places that model the four resources. Let TR1, NR1, PNR1 and VTR1 be these places. GP1 contains at least a free place PA1 modeling that A can be received, and U1={A}. 2. E2=(RP2,GP2, U2, A2); RP2={PNR2}, GP2={PA2}. 3. ψr={TR1}, ψc={VTR1}; 4. β={(PA2, str1), (PNR2, a11), (NR1, a13)}. Fig. 5 shows the configuration before firing rt. E1

PA1 str1

PA2

P11 P31

PA2

P12

rt PNR1 TR1

str3 P21

E2

PA1

str2

PNR2 a31 P32

a11 a21

P13 VTR1

P22

a12 a22 NR1 a13 a23

Figure 5: MA-model before firing rt

UbiCC Journal - Volume 3

a32

Fig. 6 shows the configuration after the firing. E2

PA2 PA1

str1 PA1

PA2

E1

str3

P11 rt

str2 PNR1

P21

VTR1

a22 P23

TR1

PNR2

a31 P32

a11

a21 P22

P12

P31

P13

VTR1

a32

a12 NR1

P4

a23 a13

Figure 6: MA-model after firing rt.

4

RECONFIGURABLE MAUDE

Maude [23] is a high-level language and highperformance system supporting executable specifications and declarative programming in rewriting logic [24]. Maude also supports equational specification, since rewriting logic contains equational logic. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Modules of Maude are theories in rewriting logic. The most general Maude module are called system modules. A rewrite theory is a triple T=(Ω, E, R), where Ω is a signature, E a set of equations and R a set of rewriting rules. The equations E in the equational theory (Ω, E) are presented as a union E=A∪E’, with A a set of equational axioms introduced as attributes of operators in the signature Ω. E’ is a set of Church-Rosser equations assumed to be terminating modulo the axioms A. Considering the Maude syntax, a system module has the form mod T endmod. Maude contains a sublanguage of functional modules and object modules. A functional module have the form fmod =(Ω, E) endfm and an object module have the same form as system module. Maude can be used as a tool for the specification and verification of distributed systems. The dynamic of the distributed system is specified by rewrite rules. Rewrite rules model transitions from one state to another state, during the execution of the distributed system. Maude has been extended to deal with some aspects not considered in former version. Real time

Page 15

Maude [25] is a system to specify and analyze real time and hybrid systems. Mobile Maude [5] is an extension of Maude for mobile systems specification. Mobile Maude is an object oriented high level language with asynchronous message passing. The key feature of mobile Maude is that it deals with various security aspects. Cryptographic authentication protects machine from malicious mobile code, redundant checks insure reliability and integrity of computations, and public-key infrastructure service protects communications. In this section we propose an encoding of Labeled Reconfigurable Nets in a Maude-based language. We call the inspired language “Reconfigurable Maude” (R-Maude). We want to profit from the powerful of Maude (as a metalanguage). We extend Maude to support the translation of LRN and their simulation. R-Maude enrich Maude with new kind of rewriting rules. Theses rules are called Reconfigurable rules (RRules). The semantic of these rules is similar to that of Reconfigurable transition in LRN. When a Rrule is executed, the R-Maude specification will be updated in different ways, this will depend on label associated with this rule. A specification in R-Maude is a set of Reconfigurable rewrite theories (R-theories). An RTheory RT is a triple (Ω, E, R) as like a rewrite theory. The different resides in the set R. R will contain two kinds of rules: standard Rules S-Rules (well known rules of Maude) and Reconfigurable rules R-Rules. A R-Rule rλ is composed of a label λ= and a rule tÆt’. In the label λ, RT1 and RT2 are two R-Theorie, S is a segment of a theory, and d a specific parameter. The segment S can be a set of sorts, rules, variables, operators that can be an R-theory or not. When rλ is fired, the specification can be updated in several ways. Updating specification means that their Rtheories will be changed. This change depends on λ. In general, when rλ is fired, the segment S will move from RT1 to RT2 or the inverse. The d parameter can be used to express direction of this move. 5

PROTOTYPING R-MAUDE

We have prototyped R-Maude. The prototype is a system composed from a text editor and an interpreter. The editor is used to enter the specification and commands. The interpreter executes commands, and through this updates specifications. The system was experimented on a LAN (Local Area Network), composed of a few machines. The system is installed on all hosts. So the specifications are edited ever where. On every hosts, commands can be executed. The execution of commands will create the system dynamic. This dynamic can be shown as migration of specification’s part (or ever else at whole) through

UbiCC Journal - Volume 3

the LAN. The specification (or their parts) are transferred in messages between machines, using UDP protocol. The interpreter realized for R-Maude can be used to interpret Maude specifications. The major different is that in this newest interpreter, we have added the interpretation of R-Rules. The label of an R-Rule precedes the rule, and it has the form [MT| L| IP@| S]. Semantics of these parameters is : MT: mobility type (MA, COD, REV, …), L: a multi-set of operations and rules to be moved, cloned or removed from or to the local host, IP@: IP address of distant host, S: sources to move or to remove from or to the local host. When specifications (or part of them) are moved, some resources (R) necessary to firing some rules become far (on an other host). IP address of the far host appears with the concerned resource in the form: R[IP@]. To encode LRN we adopt the same rules proposed to translate Petri Nets into Maude in [23]. The newest is that R-transition will be translated in R-Rules. Here after, we present the encoding of Fig.5’s example in R-Maude prototype. We consider that the two environments E1, E2 are specified as two specifications on two hosts (Host1 and Host2). Host1 has the IP address : 192.168.0.1, and Host2 has the IP address : 192.168.0.2. On Host1, we have the specification: mod E1 sort Place Marking . subsort Place << Marking . op _,_ : Marking Marking -> Marking . ops PA1,P11,P12,P13,P14,PA2,P21, P22,P23,TR1,VTR1,PNR1,NR1:->Place rl [str1] : PA1=>P11 . rl [rt][MA|192.186.0.2|{{P11P14},{str1a13}}|{TR1,VTR1}] : P11=>P12 . rl [a11] : P12, TR1, PNR1=>P13 . rl [a12] : P13, VTR1=>P14 . rl [a13] : P14, NR1=>PA1 . rl [str2]: PA2=>P21 . rl [a21] : P21, PNR1=>P22 . rl [a22] : P22, VTR1=>P23 . rl [a23] : P23, NR1=>PA2 . endmod and on Host2, we have the specification : mod E2 sort Place Marking . subsort Place << Marking . op _,_ : Marking Marking -> Marking . ops PA1,PA2,P31,P32,PNR2 : -> Place. rl [str3] : PA2=>P31 . rl [a31] : P31=>P32 . rl [a32] : P32, PNR2=>PA2 . endmod As an example of a command, we have “rw PA1” on Host1. The execution of this command

Page 16

will produce respectively on Host1, and Host2 the two specifications: mod E1 sort Place Marking . subsort Place << Marking . op _,_ : Marking Marking -> Marking . ops PA1,PA2,P21,P22,P23, VTR1,PNR1,NR1:->Place rl [str2]: PA2=>P21 . rl [a21] : P21, PNR1=>P22 . rl [a22] : P22, VTR1=>P23 . rl [a23] : P23, NR1=>PA2 . endmod and mod E2 sort Place Marking . subsort Place << Marking . op _,_ : Marking Marking -> Marking . ops PA1,PA2,P31,P32,PNR2 : -> Place. ops VTR1, TR1:-> Place. ops P11,P12,P13,P14:->Place. rl [str3] : PA2=>P31 . rl [a31] : P31=>P32 . rl [a32] : P32, PNR2=>PA2 . rl [str1] : PA1=>P11 . rl [rt][MA|192.186.0.2|{{P11P14},{str1a13}}|{TR1,VTR1}] : P11=>P12 . rl [a11] : P12, TR1, PNR2=>P13 . rl [a12] : P13, VTR1=>P14 . rl [a13]: P14,NR1[192.168.0.1]=>PA1. endmod Finally, the state of the marking will be : “P12” on the Host2. At this point, the two specifications continue their execution on the two hosts where they reside. 6

RELATED WORKS

In [4], the authors proposed PrN (Predicate/Transition nets) to model mobility. They use concepts: agent space witch is composed of a mobility environment and a set of connector nets that bind mobile agents to mobility environment. Agents are modeled through tokens. So these agents are transferred by transition firing from a mobility environment to another. The structure of the net is not changed and mobility is modeled implicitly through the dynamic of the net. In [19], authors proposed MSPN (Mobile synchronous Petri net) as formalism to model mobile systems and security aspects. They introduced notions of nets (an entity) and disjoint locations to explicit mobility. A system is composed of set of localities that can contain nets. To explicit mobility, specific transitions (called autonomous) are introduced. Two kinds of autonomous transition were proposed: new and go. Firing a go transition move the net form its locality

UbiCC Journal - Volume 3

towards another locality. The destination locality is given through a token in an input place of the go transition. Mobile Petri nets (MPN) [1] extended colored Petri nets to model mobility. MPN is based on π-calculus and join calculus. Mobility is modeled implicitly, by considering names of places as tokens. A transition can consumes some names (places) and produce other names. The idea is inherited from π-calculus where names (gates) are exchanged between communicating process. MPN are extended to Dynamic Petri Net (DPN) [1]. In DPN, mobility is modeled explicitly, by adding subnets when transitions are fired. In their presentation [1], no explicit graphic representation has been exposed. In nest nets [8], tokens can be Petri nets them selves. This model allows some transition when they are fired to create new nets in the output places. Nest nets can be viewed as hierarchic nets where we have different levels of details. Places can contain nets that their places can also contain other nets et cetera. So all nets created when a transition is fired are contained in a place. So the created nets are not in the same level with the first net. This formalism is proposed to adaptive workflow systems. In [3], authors studied equivalence between the join calculus [6] (a simple version of π-calculus) and different kinds of high level nets. They used “reconfigurable net” concept with a different semantic from the formalism presented in this work. In reconfigurable nets, the structure of the net is not explicitly changed. No places or transitions are added in runtime. The key difference with colored Petri nets is that firing transition can change names of output places. Names of places can figure as weight of output arcs. This formalism is proposed to model nets with fixed components but where connectivity can be changed over time. In this work, we have attempted to provide a formal and graphical model for code mobility. We have extended Petri net with reconfigure labeled transitions that when they are fired reconfigure the net. Mobility is modeled explicitly by the possibility of adding or deleting at runtime arcs, transitions and places. Modification in reconfigure transition’s label allows modeling different kinds of code mobility. Bindings to resources can be modeled by adding arcs between environments. It is clear that in this model created nets are in the same level of nets that create them. Creator and created nets can communicate. This model is more adequate for modeling mobile code systems. We propose also an extension for Maude, that we call R-Maude. R-Maude extends Maude with Reconfigurable rules (R-rules). When an R-Rule is fired, R-Maude specifications are reconfigured on a LAN (Local Area Net).We use R-Maude to encode and simulate LRN models.

Page 17

7

CONCLUSION

Proposed initially to model concurrency and distributed systems, Petri nets attract searchers in mobility modeling domain. The ordinary formalism is so simple with a smart formal background, but it fails in modeling mobility aspects. Many extensions were been proposed to treat mobility aspects. The key idea was to introduce mechanisms that allow reconfiguration of the model during runtime. The most works extends coloured Petri nets and borrow π-calculus or join calculus ideas to model mobility. The exchanging of names between processes in πcalculus is interpreted as exchanging of place’s names when some transitions are fired. This can model dynamic communication channels. In much formalism, mobility of process is modeled by a net playing as token that moves when a transition is fired. All these mechanisms allow modeling mobility in an implicit way. We consider that the most adequate formalisms must model mobility explicitly. If a process is modeled as a subnet, mobility of this process must be modeled as a reconfiguration in the net that represents the environment of this process. In this paper, we have presented a new formalism “labeled reconfigurable nets”. This formalism allows explicit modeling of computational environments and processes mobility between them. We have presented how this formalism allows, in a simple and an intuitive approach, modeling mobile code paradigms. We have focused on bindings to resources and how they will be updated after mobility. We have presented an extension for Maude : reconfigurable Maude (RMaude). R-Maude is a distributed system. This system can be used to specification and simulation of mobile code system. A prototype for this system has been realized. We use this prototype to encode and simulate LRN models. In our future works we plan to focus on modeling and analyzing aspects. In modeling aspects, we are interested to handle problems such that modeling multi-hops mobility, process’s states during travel, birth places and locations. On the analysis aspect, we are working on a denotational semantics for LRN. For RMaude, the current R-Maude can be used only to simulate Models. Future works will handle specification analyzing. As a future extension, we think to adapt Maude model-checker to reconfigurable Maude. In [26], we have proposed extensions for LRN “Temporal LRN”, and in [27], we proposed Coloured LRN. In this sense, we focus on using R-Maude to simulate models of these extensions.

UbiCC Journal - Volume 3

8

REFERENCES

[1] Andrea Asperti and Nadia Busi: Mobile Petri Nets. Technical Report UBLCS-96-10, Department of Computer Science University of Bologna, May 1996. [2] M.A. Bednarczyk, L. Bernardinello, W. Pawlowski, and L. Pomello: Modelling Mobility with Petri Hypernets. 17th Int. Conf. on Recent Trends in Algebraic Development Techniques, WADT’04. LNCS vol. 3423, Springer-Verlag, 2004. [3] M. Buscemi and V. Sassone: High-Level Petri Nets as Type Theories in the Join Calculus. In Proc. of Foundations of Software Science and Computation Structure (FoSSaCS '01), LNCS 2030, SpringerVerlag. [4] Dianxiang Xu and Yi Deng: Modeling Mobile Agent Systems with High Level Petri Nets. 0-7803-65836/00/ © 2000 IEEE. [5] Francisco Dur‫ل‬n, Steven Eker, Patrick Lincoln and José Meseguer: principles of mobile maude. In D.Kotz and F.Mattern, editors, Agent systems, mobile agents and applications, second international symposium on agent systems and applications and fourth international symposium on mobile agents, ASA/MA 2000 LNCS 1882, Springer Verlag. Sept 2000. [6] Cédric Fournet Georges Gonthier: The Join Calculus: a Language for Distributed Mobile Programming. In Applied Semantics. International Summer School, APPSEM 2000, Caminha, Portugal, September 2000, LNCS 2395, pages 268--332, Springer-Verlag. August 2002. [7] Alfonso Fuggetta, Gian Pietro Picco and Giovanni Vigna: Understanding Code Mobility. IEEE transactions on software engineering, vol. 24, no. 5, may 1998. [8] Kees M. van Hee, Irina A. Lomazova, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, Marc Voorhoeve: Nested Nets for Adaptive Systems. IEEE. ICATPN 2006: 241-260. [9] P. Knudsen: Comparing Two Distributed Computing Paradigms, A Performance Case Study; MS thesis, Univ. of Tromso 1995. [10] I.A. Lomazova: Nested Petri Nets. Multi-level and Recursive Systems. Fundamenta Informaticae vol.47, pp.283-293. IOS Press, 2002. [11] M. Merz and W. Lamersdorf: Agents, Services, and Electronic Markets: How Do They Integrate?. Proc. Int’l Conf. Distributed Platforms, IFIP/IEEE, 1996. [12] R. Milner: A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer Verlag, 1980. [13] R. Milner, J. Parrow, and D. Walker: A calculus of mobile processes. Information and Computation, 100:1–77, 1992. [14] Reinhartz-Berger, I., Dori, D. and Katz, S.: Modelling code mobility and migration: an OPM/Web approach. Int. J. Web Engineering and Technology, Vol. 2 (2005), No. 1, pp.6–28. [15] D. Sangiorgi and D. Walker: The π-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. [16] Athie L. Self and Scott A. DeLoach.: Designing and Specifying Mobility within the Multiagent Systems Engineering methodology. Special Track on

Page 18

Agents, Interactions, Mobility, and Systems (AIMS) at the 18th ACM Symposium on Applied Computing (SAC 2003). Melbourne, Florida, USA, 2003. [17] Tommy Thorn: Programming languages for mobile code. Rapport de recherche INRIA, N ° 3134, Mars, 1997. [18] R. Valk: Petri Nets as Token Objects: An Introduction to Elementary Object Nets. Applications and Theory of Petri Nets 1998, LNCS vol.1420, pp.125, Springer-Verlag, 1998. [19] F. Rosa Velardo, O. Marroqn Alonso and D. Frutos Escrig: Mobile Synchronizing Petri Nets: a choreographic approach for coordination in Ubiquitous Systems. In 1st Int. Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord’05. ENTCS, No 150. [20] Fernando Rosa-Velardo: Coding Mobile Synchronizing Petri Nets into Rewriting Logic. this paper is electronically published in Electronic Notes in Theoretical Computer science URL: www.elsevier.nl/locate/entcs. [21] Sutandiyo, W., Chhetri, M, B., Loke, S,W., and Krishnaswamy, S: mGaia: Extending the Gaia Methodology to Model Mobile Agent Systems. Accepted for publication as a poster in the Sixth International Conference on Enterprise Information Systems (ICEIS 2004), Porto, Portugal, April 14-17. [22] D.J. Wetherall, J. Guttag, and D.L. Tennenhouse: ANTS: A Toolkit for Building and Dynamically Deploying Network Protocols. Technical Report, MIT, 1997, in Proc. OPENARCH’98. [23] M. Clavel, F.Durán, S.Eker, P.Lincoln, N.Marti-Oliet, J.Meseguer, and J. Quesada: Maude: specification and programming in rewriting logic. SRI International, Januray 1999, http://maude,.csl.sri.com. [24] J. Meseguer: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96 (1):73-155, 1992. [25] P.C.Ölveczky, J. Meseguer: Real-Time Maude : A tool for simulating and analyzing real-time and hybrid systems. In K. Futatsugi, editor, Third International Workshop on Rewriting Logic and its Applications, volume 36 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000. http://www.elsevier.nl/locate.entcs/volume36.html. [26] Laïd Kahloul, Allaoua Chaoui: Temporal Labeled Reconfigurable Nets for Code Mobility Modeling. The International Workshop on Trustworthy Ubiquitous Computing (TwUC 2007) associated to the iiWAS2007 conference. [27] Laïd Kahloul, Allaoua Chaoui: Coloured reconfigurable nets for code mobility modeling. In the Proceedings of World Academy of Science, Engineering and Technology, Volume 25, November 2007 with ISSN: 1307-6886. WASET-XXV International Conference Venice, Italy.

UbiCC Journal - Volume 3

Page 19