ABSTRACT
The focus of this paper is on the design and development of a model translation tool for context-aware system based on the existing research outcome of Naseem [2] and
Shujun [5]. This tool, named as T2Uppaal, facilitates automatic conversion from
TADL description to Uppaal model. This paper will analyze the context aware system in TADL architecture, design the transformation rules involved context and physical properties, and present the specification of the format for input file. Moreover, this paper discusses a case study to to ensure the conversion is correct, efficient and applicabilit
ACKNOWLEDGMENTS
I would like to start off thanking my supervisor Dr.Wan for her support and guidance.
Furthermore, I am also indebted to my schoolmate Bai Wei for the help and support to this project. Finally, and most importantly, I want to thank my roommates, for the encouragement and help. This work can not exist without you.
1 Introduction
Cyber-Physical Systems (CPS) [14] are integrations of computation with physical processes, wherein networked embedded computers monitor and/or control physical processes based upon local and remote computational models. Such systems allow us to add new capabilities to physical systems. CPS has been quietly into our life. It is everywhere you look now, a common example is smart car which has the advantage of adaptability, efficiency, functionality, reliability, safety, and usability. Good performance let it be used in more domains. Correspondingly, the reliability of the system is a key issue in the system design process. There is a strong need for the use of advanced, systematic techniques and tools that support the system validation. The main work of this paper is to design and develop a model translation tool which takes a TADL design as input and transforms it into a corresponding UPPAAL timed automata model.
Modeling and verification of CPS is complicated by their heterogeneous nature as well as their sheer complexity. Architectural Description Languages (ADLs) provide a means to model and analyze software architectures in order to improve software quality and correctness. In recent years, there has been a considerable amount of research into developing ADLs. CPS can be regarded as a trustworthy component based system, and hence it could be described in Trustworthy Architectural Description
Language (TADL). There are many model checking tools in the literature, such as
UPPAAL which is a standard tool for modeling and verification of real-time systems, the basic model employed by UPPAAL is that of networks of timed automata extended with data variables. It can clearly express the system model operation and check its property such as accessibility, safety and security [3]. UPPAAL has been applied in a number of case studies. To meet requirements arising from the case studies, the tool has been extended with various features. Instead of developing new tools, to improve an existing tool is quick and simple.
For the present, Naseem Ismail Ibrahim [2] has developed transformation techniques to transform TADL descriptions into behavior protocols used by existing verification tools. The transformation rules are described independently of the transformation tool, and this allows others to extend new rules easily. However, the research object is component-based trustworthy real-time reactive system in Naseem’s thesis. Compare with a real-time system, CPS is more complex since it is usually related to context and needs to interact with physical processes through sensors and actuators. Therefore I will continus Naseem`s work and improve the transformation tool to support context.
In addition, UPPAAL also could not express continuous variables, physical properties
-1-
and other functional requirements such as context. An expansion tool of UPPAAL named as “Conpal” has been design and developed in [5]. According to this toolkit, we could reconstruct the source file of UPPAAL that add continuous variables declaration and context computation functions.
The remainder of this paper is organized as follows. Section II presents the background such as Context, UPPAAL, and TADL model. Context-aware system was represented in UPPAAL modeling and TADL architecture is discussed in section III.
The transformation from the TADL model to an UPPAAL model is discussed in Section V. We present the verification with the UPPAAL model in Section VI. Section
VII briefly introduces the learning points in this project. Finally, Section VII discusses professional issues.
2 Background
2.1
UPPAAL
UPPAAL [3] is an integrated tool environment for modeling, simulation and verification of real time system. It is appropriate for systems that can be modeled as networks of timed automata [13], i.e. a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels and shared variables. We refer the reader to [3] for a more thorough description of the timed automata used in UPPAAL. The application of UPPAAL has shown particular advantages in aspect of real-time systems, such as analysis of communication protocols, operation of train systems. The syntax used for declarations in UPPAAL is similar to the syntax used in the C programming language. We present some of the features that are relevant to this paper:
Global variables: This section contains global variables, clocks, synchronization channels, constants, and user defined function. The inclusion of all these variables and functions can be accessed by all templates.
Template: Time automata are defined with a set of local variables, and these local variables should be initialized during template declaration.
Committed Location: In a committed location, time is not allowed to pass, and the next transition must include an outgoing edge of at least one of the committed locations.
Binary synchronization: A synchronized transition means when an event occurs two timed automata move to new state at the same time. The channels are declared to represent the event (labeled with? and!).
-2-
Arrays: All of clocks, channels, constants and integer variables can be declared as an array, for example, int xLoc [0, 5].
Constants: It is used to definition a parameter which the value cannot be modified. The parameter is declared as const name value.
Expressions: There are three main types of expressions:
a) Guard expressions which include clocks and state variables are used to restrict the behavior of transitions between locations. This is a Boolean expression.
b) Assignment expressions are used to assign values to clocks and variables at the edges.
c) Invariant expressions are used to define conditions that should be always true in a location.
Edges: Edges define transitions between locations. Each edge consists of four expressions: a) Select, which assigns a value to a defined variable in a given range
b) Guard, which checks an edge that it is enabled if the guard expressions are true c) Synchronization, which specifies the synchronization channel and its direction
d) Update: whichs reset variables and clocks to required values by an assignment statements
2.2
TADL
Trustworthy Architectural Description Language (TADL) is a novel architecture description language for describing the architecture of trustworthy component-based systems and developed by Mohammad and Alagar [7]. The goal of TADL is to achieve a uniform specification language for specifying and analyzing the different kinds of trustworthiness properties such as safety, security, and real-time schedulability analysis to ensure timelimess.
A meta-model is used to model architectures by defining types from which system architecture can be defined. Figure 1, which is taken from [7], shows the component model that explains the set of related models. The main elements of this meta-model included: Component definition, Architecture definition, Safety contract, Security mechanism, System definition, Attribute, Constraint and Package.
-3-
Fig.1 Meta-model
2.3
Context Aware
Context is the physical and social situation in which the person device is a part of, it can be divided into two categories external and internal. External context, sometimes also called physical context, can be measured by hard ware sensors such as location, light, sound, movement, touch, temperature, air pressure, etc. In contrast, the internal context is mostly specified by the user or captured monitoring the user’s i nteraction, like the user’s goal, tasks, work context, business processes, the use’s emotional state, etc. Dey & Abowd [10] have been redefined the terms “context”,
Any information that can be used to characterize the situation of entities (i.e. whether a person, place or object) that are considered relevant to the interaction between a user and an application, including the user and the application themselves.
In computer science context awareness refers to acquire and utilize context from a computer device in order to provide services that are appropriate given the acquired context. Aim at increasing usability and effectiveness by taking environmental context
-4-
into account, context-aware systems are able to adapt their operations to the current context without explicit user intervention. Figure 2 shows the softeware architecture for context-aware system.
Sensor
Mechanism
Data
Store
Context
Mechanism
ContextAware
System
Reactivity
Mechanism
Adaptation
Mechanism
Service
Mechanism
Fig.2 The softeware architecture for Context-Aware System
3 Design
This section discusses the TADL and UPPAAL models representing the Context-aware system. In order to formalize the structure of TADL model, we started with defined TADL XML scheme. A detailed description of the transformation rules was also presented.
3.1
Context in UPPAAL
Conpal [5] extend the UPPAAL formal template by adding context mechanism.
In the global declaration section, it has defined
Dimension typedef struct
{
int Tag; int Value;
}Context;
Context
Context was represented by an array of dimensions, for example
Context LocationContext[NUM];
-5-
Context Data Set
According to the software architecture for Context-Aware Systems, data storage is necessary for adaptation mechanism to query and retrieval context data. struct{ int XCoord; int YCoord; int SightName;
}Map[12] =
{{1,4,BONE},{2,4,BONE},{1,1,BTHREE},{1,2,BTHREE},{2,1,BTHREE}
,{2,2,BTHREE},{3,1,BTWO},{4,1,BTWO},{3,2,BTWO},{4,2,BTWO},{3,
4,BA},{4,4,BA}};
Context Build Function
For details, see the appendix C.
Context Calculate Function
There are there context operation were performed including Projection, Intersection and Union, the detail of these algorithms will be given in the Appendix C.
Adaption Function
The specific context is mapped to a guard value by using this function, where value is a parameter of the template. For details, see the appendix C.
3.2
Context in TADL
We have extended Figure 1 with context inclusion. The following parts provide a detail explanation of the difference between original and extened architectures.
3.2.1 Context mechanism
A context property is concerned with functional requirements for context aware system, such as the context structure, and the context computation functions which are essential for systems adaptation. It is also possible to define database which are used for context adaptation.
-6-
Fig.3 Context mechanism
3.2.2 Safety Contract
A safety property [2] is considered a contract on a component type. A new optional context constraint has been added to a contract. A context constraint is generally accepted as a condition which must be satisfied to enable the reactivity property. It is very similar to a data constraint which defined the values of the context parameters for the same stimulus to responses differently. An example of a context constraint would be: if the current temperature (context) is more than 30 centigrade, the controller will lower (a response) the temperature.
Fig.4 The safety contract
-7-
3.2.3 Physical property
A physical property is the concerning the context. It is a special attribute and used to define continuous variables that can be associated with context elements. It is possible for the physical property to have an assigned range of value.
3.3
Transformation rules
We extend the transformation rules by adding context support.
A context-aware system is translated to a UPPAAL model.
Context-Aware System
ComponentType
UPPAAL Model
Hardware Compo-
nents
Global declaration
Role Assignments
Templates
Groups Assignments
Local Declarations
Deployment
ContextType
System Declaration
Physical
Fig.5 TADL to UPPAAL
In a component-based system, each component can be mapped to a UPPAAL template in one to one manner [7].
ComponentType
UPPAAL template
ContractTypes
Constraints
Context
Edges Expressions:
Attributes
InterfaceTypes
Actions
ArchitectureTypes
Location
1.
Select
2.
Guard
3.
Sync
4.
Update
Invariants
Clock
Fig.6 Component to template
-8-
Transformation rules in Contract
The contract is one of elements in a component and used to define the behavior of this component. Context constraints were added. The context parameter may be necessary for service type.
ContractType
UPPAAL template
1.
2.
Service-Response
Actions
Service-Request
Location
Reactivity Rule
Edges Expressions:
Used in Guard
Reactions
Context Constraint
Time Constraint
Guard
Sync
4.
Data Constraint
conditions
Select
2.
Update
1.
3.
Update
Invariants
Clock
Fig.7.ContratctType transformation
Transformation rules in Context Type
The global declaration includes the context mechanism. The ContextType defines context properties and functions in the TADL model.
Context Type
UPPAAL Model
Dimension
DataSet
Function
Global declaration
Templates
Local Declarations
System Declaration
Fig.8 ContextType transformation
-9-
The context properties are transformed to the global declaration using the following rules: Creat a struct of context representing the dimension that obtained from the ContextType dimension list.
Create arrays of context dimension which declare the context variables.
Create a data access control set which defines the tuples(x, y, tag).
Define a context build function
Define some context operation function, which calculates the context
Define an adaption function, which searchs the context data set and returns which service the system adapted.
4 Realization
In this section the rules and process for transforming a context aware system described using the TADL model to the UPPAAL model are presented. The full contents of the transformation rules can be found in Appendix B. Below are a detailed discussion of the extended transformation tool. Figure 9 presents the transformation process from TADL model to UPPAL. In order to achieve that, the DTD defined the logic frame, the XML described the system, the XSD gave the format, and the XSLT defined the transformation rules.
TADL Model
VMT
TADL Schema
UPPAAL.xml
TADL.xml
T2UppAal
Verification
UppAal
Transformation rules
Fig.9 Transformation Process
4.1
DTD and XML schemas
4.1.1 UPPAAL XML DTD
Figure 10 shows the DTD schema for the UPPAAL XML file. The XML should contain three elements, , and , under the root element
. The element also contain the local , and
.
- 10 -
Fig.10 UPPAAL XML DTD
4.1.2 TADL XML schemas
The XML schemas for representing the TADL model should be defined before implement the transformation rules. We will modify the Naseem`s XML schemas in order to add more elements and structures to our model.
- 11 -
ContextType file: This file contains the contextType and architecture definition. Each context may have a name, a list of dimensions, a capacity, a database, a list of fun ctions and a description. Each database contains a name, a list of attributes, a list of data and a description. Figure 11 shows the XML schema for defining ContextType.
The content of this file can be found in Appendix A.
...
Fig.11 ContextType Schema
PhysicalType file: This file contains the Physical property and architecture definition.
Each physical type may have a name, a datatype, a maximum value, a minimum value and a description.
Fig.12 PhysicalType Schema
ContractType file: This file may add a context constraint, and an operation element.
- 12 -
Figure 13 shows the revised part of the ContractType schema. The full content of this file can be found in Appendix A.
...
...
Fig.13 ContractType Schema
ComponentType file: This file may add a context element. The full content of this file can be found in Appendix A.
4.2
Transformation rules in XSLT
The transformation rules are implemented in a XSLT file. A UPPAAL xml file is comprised of global declaration section, templates section, and system declaration.
According to such structure, the XSLT file may contain the definitions of creating the global declaration, the rules for transforming each component into a template, and the definitions for the system-level declaration. We will give the detail in the next.
4.2.1 Global declaration
To achieve the support for context aware, the global declaration rules are responsible for generating the context declaration for the UPPAAL system. It will contain:
The definition of the context mechanism, which includes:
a) a context struct, which define the dimension of context
b) a database declaration, which represent the context data set
- 13 -
c) the functions, which include context build function, context calculate function, and adaption function
The context variables, which are transformed from the TADL system level attributes
The physical variables, which are transformed from continuous variables to bounded discrete variables.
Below is a more detailed discussion.
Fig.14 Context data set transformation rules
- 14 -
Fig.15 Physical property transformation rules
Fig.16 Dimmension transformation rules
Fig.17 Context variables transformation rules
- 15 -
Fig.18 Context function transformation rules
4.2.2 Template
Each component can be mapped to a UPPAAL template in one to one manner. When the contract type has been modified, Figure 19 shows the transformation rules for creating context constraint, and Figure 20 shows the transformation rules for creating the assignment statements. It is worthwhile to note that a component may have a context.
In that case the context will be represented in local declaration same as global declaration, we will not repeat again.
Context Constraint in Contract
The full contents of the transformation rules can be found in Appendix B.
4.3
T2UppAal
This paper realizes the T2UppAal as a new version of Transformation Tool [2] with a slight revision by the development environment of NetBeans IDE 7.1.1. The function related to the TIME model has been removed. It contains four classes as show below.
TransformationTool class: The main class contains the implementation of the
GUI and the transformation process.
TreeBuilder class: This class is used to define a Tree view of an XML file.
XmlFilter class: This class is used for filtering XML files when opening or saving the input or output of the transformation tool.
XsltFilter class: This class is used for filtering XSLT files when transforming the object file.
Figure 21 shows a view of the tool. The “Open” button is used to open an input
TADL XML file, and the input file will be displayed in the above panel with text view or tree view. To perform the transformation, the “Transform” button should be clicked. After complete the transformation process, the output file will be displayed in the below panel and the “Save” button will be active to save the transformation result.
- 17 -
Fig.21 T2UppAal Main View
5 Testing & Evaluation
In this section a simple case study will be present to illustrate the specification of the transformation rules proposed by this paper. First, the TADL presentation of the case study is presented. Then, the UPPAAL presentation and the system properties were discussed during verification. Finally an analysis of the project strength and weakness was presented.
5.1
Case Study
Tourist guide system (TGS) (taken from [5]) is a handheld device designed to provide pre-recorded spoken commentary to a visitor in Xi`an Jiaotong-Liverpool University
(XJTLU) without user interaction. Figure 22 shows a simple map of XJTLU, the campus basically consists of four parts, Building 1( Fundamental Teaching & Learning Building), Building 2(Science & Research Building), Building 3(Administration and Learning Resource Building) and A 4&5(Self-study and Business Building). For
- 18 -
the different area, the Tour Guide will play different audio interpretation. Many of us have experienced the similar problem. We want to build a context-aware tourist guide system Building 1
A 4&5
Building
3
Building 2
Fig.22 a simple map of XJTLU
In this system, the contexts refer to the geographical location of the user. Therefore a plane coordinate system should be built based on the above map before we design the TGS in the TADL model.
5
Building 1
Y-coordinat
4
A 4&5
3
2
Building 3
Building 2
1
0
0
1
2
3
4
5
X-coordinate
Fig.23 A plane coordinates system
- 19 -
It can be seen from the Figure 23 that Building 1 can be identified by the coordinates
(1, 4) and (2, 4); Building 2 can be identified by the coordinates (3,1), (4,1), (3,2) and
(4,2); Building 3 can be identified by the coordinates (1,1), (1,2), (2,1) and (2,2);
Building A4&5 can be identified by the coordinates(3,4) and (4,4). After that we are beginning to design this system, the description language is TADL. TGS consists of a sensor component that collects the current user location coordinate(x, y) and sends it continuously to a processor component. Upon receipt of the location coordinates, the processor will process the location information in order listed in the below:
[1]. Build context dimension;
[2]. Build location context;
[3]. Compare with the last location context, and then build the change context.
[4]. Union operation perform between Change Context and Location Context to produce the Guider Context
[5]. Send the Guider Context to the adapter.
Then the adapter will manage the guider context according to adaption function and issue a command to Audio to play a corresponding audio file. The system also includes an operation component which the inclusions of all the users are allowed to switch the system on and off.
5.1.1 TADL Representation
The following describes the system using TADL. Firstly, varied variables were defined include physical parameter, data parameter and context parameter.
PhysicsType xLocation {
DataType = int;
}
ParameterType Changed{
DataType = int;
}
ContextType LocationContext { xLocation xLoc; yLocation yLoc;
}
ContextType GuiderContext{
Changed changed
}
...
Fig.24 A part of the parameters definition
Secondly the services provided in this system are defined.
- 20 -
ServiceType CurrentXLocation { yLocation ycurrent;
}
ServiceType CurrentYLocation { xLocation xcurrent;
}
ServiceType BuildLocationContext{
}
ServiceType GetGuiderContext{
}
ServiceType adaptGuider{
Context guiderContext;
}
ServiceType PlayB1 {
Context b1;
}
ServiceType Stop {}
ServiceType ON {}
ServiceType OFF {}
Fig.25 A part of the Severic definition
TimeConstraint TCAdaptGuider {
CurrentXLocation Xcurrent;
RequestService(Xcurrent);
adaptGuider adaptguider;
ResponseService(adaptguider);
float MaxSafeTime = 5;
}
DataConstraint DCCurrentXLocation{
XLoction x;
RequestService(x);
CurrentXLoction current
ResponseService(current);
0
