A model for Real-time concurrent interaction protocols in component interfaces

Download

VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

A Model for Real-time Concurrent Interaction Protocols

in Component Interfaces

Van Hung Dang^∗, Trinh Dong Nguyen, Hoang Truong Anh

VNU University of Engineering and Technology, Hanoi, Vietnam

Abstract

Interaction Protocol specification is an important part for component interface specification. To use a

component, the environment must conform to the interaction protocol specified in the interface of the

component. We give a powerful technique to specify protocols which can capture the constraints on temporal

order, concurrency, and timing. We also show that the problem of checking if a timed automaton conforms to a

given real-time protocol is decidable and develop a decision procedure for solving the problem.

Received 16 January 2017; Accepted 27 February 2017

Keywords: Interaction Protocol, Timed Automata, Region Graph, Component Interface.

1. Introduction^*

An interaction protocol specified in the

interface of a component is a precondition on

the temporal order on the use of services from

the component. Fail to satisfy this precondition

may lead to a system deadlock [2]. In real-time

systems, when a service from a component

takes a considerable time to carry out, too

frequently calling to this service may lead to the

error state too. So, we need to specify the

minimum duration between two consecutive

calls to the services that takes time, and this

also plays a role of precondition on the

consecutive calls to those services in the

interaction protocols. Another possibility that

we need to consider when specifying this kind

of time constraints is that a component may be

able to provide services in parallel. In this case,

Component-based system architectures

have been an efficient divide-and-conquer

design technique for the development of

complex real-time embedded systems. A key

role in this technique is component interface

modeling and specification. There have been

many significant progresses towards

comprehensive theory for interfaces, see for

example [2, , 3, 5, 6, 7]. In those works

different aspects of interfaces have been

modeled and specified such as interaction

protocols, contracts, concurrency, relations,

synchnony and asynchrony. An approach that

integrates all those aspects has been introduced

in [4]. However, there has not been an intuitive

and powerful model for real-time interaction

protocols. This kind of model plays an crucial

role in systems where a service from a

component may take long time to finish.

time

constraints

not

apply

concurrent services.

Let us consider an example. Imagine that

we have a software component that provide

accesses to two files: one stores the information

about products and the other stores the

information about customers. To access to a

_______

^*Corresponding author. E-mail.: dvh@vnu.edu.vn

https://doi.org/10.25073/2588-1086/vnucsce.154

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

file, one needs to open it, and after use one

needs to close it. Accesses to different files can

be done in parallels, and access can be reads

and writes such that all the reads should be

2. General protocol model

Let Σ_푖, ꢀ = 1, … , 푘 be alphabets of service

푘

names for a component ꢁ, and let Ω =

Σ_푖

⋃

푖=1

before writes. Let us denote by 푂_푝, 푅_푝, 푊 and

퐶_푝the accesses open, read, write and close for

be the alphabet of all service names that the

component provides. Our intention is that

services in each Σ_푖need to be executed

sequentially, and services in different Σ_푖and Σ_푗

푝

the file 1 (for products), and by 푂_푐, 푅_푐, 푊 and

푐

퐶_푐the accesses open, read, write and close for

the file 2 (for customers). To use the component

we need to activate it by action 퐴, and we need

to deactivate it by action 퐹 after use. The

interaction protocol could be specified by two

regular expressions to express the condition on

the temporal order between actions on each file.

can be executed in parallel. Each Σ_푖, ꢀ = 1, … , 푘

can overlap another, but they must not be

included in each other, i.e. Σ_푖is a maximal set

of services that need to be executed in

sequence. When 푘 = 1 there is no concurrency

for the component. Each service in Ω may take

time to finish. We specify this fact by a

function 훿: Ω → ℝ^≥. So, a service 푎 ∈ Ω takes

훿(푎) time units to finish. An interaction

protocol specifies a constraint on the temporal

order on the services in each separate Σ_푖, and

this is modeled efficiently by a regular

expression on Σ_푖. Therefore, we define:

These

regular

expressions

could

(퐴(푂_푝푅_푝푊 퐶_푝)^∗퐹)^∗and (퐴(푂_푐푅_푐푊 퐶_푐)^∗퐹)^∗.

푝

푐

Does the execution 퐴푂_푝푂_푐푅_푝푅_푐푊 푊 퐶_푝퐶_푐퐹

푐

푝

conform to this protocol? It does because it

satisfies the restriction on the temporal order for

each file. Now, assume that it takes 1 second

for the read accesses, then the execution will

satisfy the protocol if the delays between 푅_푝

Definition

protocol) A real-time interaction protocol 휋 is a

tuple 〈(훴₁, 푅₁), … , (훴_푘, 푅_푘), 훿〉, where

훴_푖→ ℝ^≥, and 푅_푖is a regular expression

(Real-time interaction

and 푊 (not 푅_푝and 푅_푐; these can be done in

푝

parallel), and 푅_푐and 푊 are more than 1

푐

second.

푘

푖=1

훿:

⋃

In this work, we propose a technique to

specify real-time concurrent interaction

protocols for component interfaces that is an

efficient formalization of the specification from

the example mentioned above, and define

formally what we mean by saying a real-time

execution conforms to an interaction protocol in

our model. Then we develop a technique to

check if a real-time system modeled by a timed

automaton satisfies a real-time concurrent

interaction protocol specified in the interface of

a component.

on 훴_푖for ꢀ = 1, … , 푘.

Example. In the example introduced in the

Introduction of this paper,

(Σ₁, 푅₁) = ({퐴, 푂_푝, 푅_푝, 푊 , 퐶_푝, 퐹},

푝

(퐴(푂_푝푅_푝푊 퐶_푝)^∗퐹)^∗) 푎푛푑,

푝

(Σ₂, 푅₂) = ({퐴, 푂_푐, 푅_푐, 푊 , 퐶_푐, 퐹},

푐

(퐴(푂_푐푅_푐푊 퐶_푐)^∗퐹)^∗).

훿(푅_푝) = 훿(푅_푐) = 1, and 훿(푋) = 0 for all

푐

other services 푋.

Let, in the sequel, for the simplicity of the

presentation, for a regular expression 푅 we

overload 푅 to denote also the language

generated by 푅, and when 푅 is the language

generated by 푅 can be understood from the

context. Note that a regular expression can

always be represented by an automaton.

This definition gives a simple syntax

representation for real-time protocols. To

understand the meaning of this representation

The paper is organized as follows. The next

section presents our general model for real-time

concurrent interaction protocols. Section 3

presents an algorithm to check if a timed

automaton satisfies a protocol specification.

The last section is the conclusion of our paper.

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

we need to define what to mean by saying a

real-time execution conforms to a protocol in

our model. We will use a timed automaton as

our system model, and therefore, use a timed

language to represent the behavior of

our system.

A timed word over an alphabet Ω is a

sequence 푤 = (푎₁, 푡₁)(푎₂, 푡₂) … (푎_푛, 푡_푛), where

푡_푖−1≤ 푡_푖for 0 < ꢀ ≤ 푛, 푡₀= 0. The intuition

of this representation for a behavior is that the

action 푎_푖takes place at time 푡_푖. Given a

protocol 휋 as in Definition 1, how to mean that

system, in order to use the services from ꢁ, all

the accepted behaviors of the system design

need to conform to 휋. The best model of real-

time systems is timed automata model [1] to the

best of our knowledge. Now the question of the

pluggability of a real-time environment to

component ꢁ is to decide whether all the

members of the timed language of a given

timed automaton ꢃ conform to the protocol 휋.

If it is the case, we write ꢃ ⊧ 휋 for short.

푤

conforms to 휋? Let us denote

3. Checking the pluggability

푢푛푡ꢀ푚푒푑(푤) = 푎₁푎₂… 푎_푛. For a word 푥 ∈ Ω^∗

we denote 푥|_Σthe projection of 푥 on Σ_푖, i.e. the

word obtained from 푥 by removing all the

characters that do not belong to Σ_푖.

Definition 2 (Conformation) A timed

word 푤 = (푎₁, 푡₁)(푎₂, 푡₂) … (푎_푛, 푡_푛) conforms

protocol 휋, denoted by 푤 ⊧ 휋, iff for all ꢀ ≤ 푘

In this section we present a technique to

solve the problem mentioned in the last section.

Namely, we will prove that it is decidable if all

the accepted behaviors of a timed automaton ꢃ

conform to a real-time concurrent interaction

protocol 휋. Then we develop an algorithm to

check if ꢃ ⊧ 휋. The algorithm serves for

answering the question if the component ꢁ can

fit to our design. For simplicity, we now restrict

ourselves to the case that the value of function

훿 in 휋 is integers.

Since the concept of timed automata may

not be familiar to some readers, we recall this

concept from [1]. A timed automaton is a finite

state machine with an additional set of clock

variables 푋 and an additional set of clock

constraints. A clock constraint 휙 over 푋 is

defined by the following grammar:

ꢂ

1. 푢푛푡ꢀ푚푒푑(푤)|_Σ∈ 푅_푖, and

ꢂ

2. let 푢푛푡ꢀ푚푒푑(푤)|_Σ= 푎_푗… 푎_푗, then

ꢂ

푚

ꢂ

푡_푗− 푡_푗≥ 훿(푎_푗) for all 푙 < 푚_푖.

푙+1

푙

The first condition in the definition says

that the temporal order between sequential

services is allowed by the component and reach

an acceptance state of the component, and the

second condition says that the component has

been given enough time for providing the

services. According to this definition, the

behavior

(퐴, 0)(푂_푝, 0)(푂_푐, 0)(푅_푝, .5)(푅_푐, 1)(푊 , 2)

휙 =̂ 푥 ≤ 푛 | 푥 ≥ 푛 | ¬휙 | 휙₁∧ 휙₂,

where푥 ∈ 푋 and 푛 stands for a natural

number. Let Φ(푋) denote the set of all

clock constraints over 푋.

Definition 3 (Timed automata) A timed

automaton 푀 is a tuple

푐

(푊 , 2)(퐶_푝, 2)(퐶_푐, 2)(퐹, 3)

푝

conforms to the protocol in Example 2.

However,

(퐴, 0)(푂_푝, 0)(푂_푐, 0)(푅_푝, .5)(푅_푐, 1)(푊 , 1.5)

푐

(푊 , 2)(퐶_푝, 2)(퐶_푐, 2)(퐹, 3)

푝

〈퐿, 푠_퐼, Σ, 푋, 퐸, ℱ〉, where

does not as 1.5 − 1 < 훿(푅_푐).

• 퐿is a finite set of locations,

• 푠_퐼∈ 퐿is an initial location,

• Σ is a finite set of labels,

• 푋is a finite set of clocks,

From the semantics of a protocol 휋, when

no services can be executed in parallel 푘 = 0,

and when there is no constraint for temporal

order on Σ_푖and acceptance state the regular

expression 푅_푖= Σ_푖^∗.

• 퐸 ⊆ 퐿 × Σ × Φ(푋) × 2^푋× 퐿is a finite set

of transitions. An 푒 = 〈푠, 푎, 휙, 휆, 푠′〉 ∈ 퐸

represents a transition from location 푠 to

Given a component ꢁ with the protocol

specification 휋 in its interface, a design of a

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

location푠′, labeled with 푎; 푠 and 푠′ are

called source and target locations of 푒, and

denoted by 푒⃖and푒⃗respectively; 휙 is a clock

constraintover 푋 that must be satisfied

when the transition 푒 is enabled, and 휆 ⊆ 푋

is the set of clocks to be reset by 푒 when it

takes place. In the sequel, we will use the

subscript 푒 with 휙 and 휆 to indicate that 휙

satisfies 휙_푒for all 1 ≤ ꢀ ≤ 푚, where 휈_푖=

ꢂ

[휆_푒↦ 0](휈_푖−1+ 휏_푖− 휏_푖−1) for 1 ≤ ꢀ ≤ 푚.

ꢂ

So, a behavior 휎 expresses that 푀 starts

from the initial location 푠_퐼, transits to 푒⃗⃗⃗⃗by

taking 푒₁at time 휏₁, then transits to 푒⃗⃗⃗⃗ by

taking 푒₁at time 휏₂, and so on, and at last

transits to 푒⃗⃗⃗⃗⃗⃗ at time 휏_푚. Note that (휈_푖−1

푚

휏_푖− 휏_푖−1) is the value of the clock variables

just before 푒_푖’s taking place, and 휈_푖is the value

of the clock variables just after 푒_푖’s taking

place. The behavior 휎 expresses also that the

system 푀 stays in the location푒⃖⃗⃗_푖for 휏_푖− 휏_푖−1

and

휆

are

associated

to 푒.

• ℱ ⊆ 퐿is the set of acceptance locations.

In this paper, for simplicity, we only

consider the deterministic timed automata, i.e.

those timed automata which do not have more

than one 푎-labeled edge starting from a location

푠 for any label 푎 ∈ Σ.

time units, and then transits to by 푒⃖⃗⃗⃗⃗⃗⃗⃗for (1 ≤

ꢀ ≤ 푚). If 휎 = (푒₁, 휏₁)(푒₂, 휏₂) … (푒_푚, 휏_푚) is a

푖+1

behavior of timed automaton 푀, we call 푒⃗⃗⃗⃗⃗⃗ a

푚

reachable location of 푀 and 〈푒⃗⃗⃗⃗⃗⃗, 휈_푚〉 a

푚

(discrete) reachable state of 푀. A behavior of

A clock interpretation 휈 for a set of clock 푋

is a mapping 휈: 푋 → 푅푒푎푙푠, i.e. 휈 assigns to

each clock 푥 ∈ 푋 the value 휈(푥). A clock

interpretation represents the values of all clocks

in 푋 at a time point. We adopt the following

denotations. 휈₀always denotes the clock

interpretation which maps from 푋 to {0}. For a

clock interpretation 휈 and for 푡 ∈ 푅, 휈 + 푡

denotes the clock interpretation which maps

each clock 푥 ∈ 푋 to the value 휈(푥) + 푡. For 휆 ⊆

푋, [휆 ↦ 0]휈 is the clock interpretation which

assigns 0 to each 푥 ∈ 휆 and agrees with 휈 over

the rest of the clocks.

A state of a timed automaton 푀 is a pair

〈푠, 휈〉, where 푠 ∈ 퐿 and 휈 is a clock

interpretation for 푋. The fact that 푀 is in a state

〈푠, 휈〉 at a time instant means that 푀 stays in

location 푠 with all clock values agreeing with 휈

at that instant.

timed automaton 푀 is accepted iff 푒⃗⃗⃗⃗⃗⃗ ∈ ℱ. Let

푚

푠_푖= 푒⃗⃗⃗_푖, for 1 ≤ ꢀ ≤ 푚, and 푠₀= 푠_퐼. Then the

run corresponding to 휎 is the sequence:

푒

〈푠₀, 휈₀〉 →_휏〈푠₁, 휈₁〉 →_휏…

푒

푚

→

〈푠_푚, 휈_푚〉.

휏

푚

The finite language of 푀 is the set of all

accepted behaviors of 푀.

In order to solve the emptiness problem for

a timed automaton, Alur and Dill [1] have

introduced a finite index equivalence relation

over the state space of the automaton. The idea

is to partition the set of the clock interpretations

into a number of regions so that two clock

interpretations in the same region will satisfy

the same set of clock constraints.

For each 푥 ∈ 푋, let 퐾_푥be the largest integer

constant occurring in a clock constraint for the

clock variable 푥 of the timed automaton 푀, i.e.

{ |

퐾_푥= max 푎 푒ꢀ푡ℎ푒푟푥 ≤ 푎 or

The behavior of timed automata can be

represented by timed words (or timed-stamped

transition sequences). A behavior 휎 is a timed

word

푥 ≥ 푎occursinaclockconstraint

of휙ofatransition푒 }.

Let 퐾_푋= max_푥∈푋퐾_푥.

For a real number 푟, let 푓푟푎푐(푟) = 푟 − ⌊푟⌋

(⌊푟⌋ is the maximal integer number which is not

greater than 푟) be the fractional part of 푥. The

equivalence relation ≅ over the set of clock

interpretations is defined as follows: for two

clock interpretations 휈 and 휈′, 휈 ≅ 휈′ iff the

following three conditions are satisfied:

휎 = (푒₁, 휏₁)(푒₂, 휏₂) … (푒_푚, 휏_푚), where 푚 ≥

1 and 푒_푖∈ 퐸, 푒⃗⃗⃗⃗⃗⃗⃗⃗ = 푒⃖⃗⃗_푖for 1 ≤ ꢀ ≤ 푚 (with the

푖−1

convention 푒⃗⃗⃗⃗ = 푠_퐼), and where 0 = 휏₀≤ 휏₁≤

휏₂≤ ⋯ ≤ 휏_푚, such that (휈_푖−1+ 휏_푖− 휏_푖−1

)

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

1. For all x ∈ X either ν(x) > K_x∧ ν′(x) >

K_xor ⌊ν(x)⌋ = ⌊ν′(x)⌋.

2. For all x, y ∈ X such that ν(x) ≤ K_xand

ν(y) ≤ K_y, frac(ν(x)) ≤ frac(ν(y)) iff

frac(ν′(x)) ≤ frac(ν′(y)).

푀〈푠, 푎, 휙, 휆, 푠′〉 such that 훼′ satisfies

휙and 훽 = [휆 ↦ 0]훼′,

• ℱ′ ⊆ 퐿′such that 푠′ ∈ ℱ′ iff 푠′ = 〈푠, 훼〉

where 푠 ∈ ℱ and 훼 is a clock region.

3. For all x ∈ X such that ν(x) ≤ K_x,

frac(ν(x)) = 0 iff frac(ν′(x)) = 0.

Note that ℛ(푀) is a ‘untimed’automaton,

and we also denote its (untimed) language

by ℒ(ℛ(푀)).

When 휈 ≅ 휈′, it is not difficult to see that

We can simplify the automata 푀 and ℛ(푀)

such that all states (locations) are reachable and

all states can lead to an acceptance state.

We recall some results from the timed

automata theory [1] that will be used in our

checking procedure later. Let ℒ(푀) denote the

휔-timed language (language of infinite timed

words) generated by 푀 (by adding 휀-transitions

from a final state to itself we can extend the

finite language of 푀 to the 휔 language).

Theorem 1

for any clock constraint 휙 occurring in a

transition 푒 = 〈푠, 푎, 휙, 휆, 푠′〉 ∈ 퐸, 휈 satisfies 휙

iff 휈′ satisfies 휙.

A clock region for 푀 is an equivalence

class of the clock interpretations induced by ≅.

We denote by [휈] the clock region to which a

clock interpretation 휈 belongs. From the

definition of ≅, a region is characterized by the

integer part of the value of each clock 푥 when it

is not greater than 퐾_푥, by the order between the

fraction part of the clocks when they are

different from 0. Therefore, the number of

1.For the timed automaton 푀,

푢푛푡ꢀ푚푒푑(ℒ(푀)) = ℒ(ℛ(푀)). Therefore,

clock regions is bounded by |푋|! ⋅ 2^|푋|

⋅

the emptiness problem for 푀 is decidable.

∏

(2퐾_푥+ 2). A configuration is defined as

푒

휏

… →^푒_휏〈푠_푚, 휈_푚〉is

푥∈푋

푚

〈

〉

〈

〉

푠₁, 휈₁→

2. If 푠₀, 휈₀

→

휏

a pair 〈푠, 훼〉 where 푠 ∈ 퐿 and 훼 is a clock

region. Based on the clock regions, the region

automaton of 푀, whose states are

configurations of 푀, and whose transitions are

the combination of a time transition and a

action transition from 푀. There is a time

transition from 〈푠, 훼〉 to 〈푠, 훽〉 iff 훽 = 훼 + 푡 for

some 푡 (here for 훼 = [휈] we define 훼 + 푡 =

[휈 + 푡]).

Definition 4 (Region automata) Given a

timed automaton 푀 as in Definition 3, the

region automaton of 푀 is the automaton

ℛ(푀) = 〈퐿′, 푠′_퐼, 훴, 퐸′, ℱ′〉, where

a run from the initial state of 푀 then

〈푠₀, [휈₀]〉 →^푒〈푠₁, [휈₁]〉 →^푒… →^푒〈푠_푚, [휈_푚]〉

푚

is a run of ℛ(푀), and reversely, if

〈푠₀, [휈₀]〉 →^푒〈푠₁, [휈₁]〉 →^푒… →^푒〈푠_푚, [휈_푚]〉

푚

is a run in ℛ(푀) then there are 휏₁, … , 휏_푚

such

that

〈푠₀, 휈₀〉 →^푒〈푠₁, 휈₁〉 →^푒… →_휏^푒〈푠_푚, 휈_푚〉 is

푚

휏

푚

a run from the initial state of 푀.

Let in the sequel, for an automaton 푀 the

size of 푀 (the number of transitions and

locations) be denoted by |푀|.

Now, we return to the problem to decide if

푢푛푡ꢀ푚푒푑(ℒ(ꢃ))|_Σ⊆ 푅_푖for a given timed

• The set of states 퐿′ consists of all

configurations of 푀,

• 푠′_퐼= 〈푠_퐼, [휈_휃]〉where휈_휃is the clock

valuation that assigns 0 to all clock

variables in 푋,

ꢂ

automaton ꢃ. It turns out that this problem is

solvable, and just a corollary of Theorem 1.

Theorem 2 Given a regular expression 푅_푖

and a timed automaton ꢃ the problem

푢푛푡ꢀ푚푒푑(ℒ(ꢃ))|_훴⊆ 푅_푖is decidable in

풪(|ℛ(ꢃ)|. |푅_푖|) time.

Proof. Let ℬ be an automaton that

recognizes all the strings on Σ_푖that do not

belong to 푅_푖, i.e. an automaton that recognizes

• 퐸′ is the set of transitions of ℛ(푀) such

that a transition ((푠, 훼), 푎, (푠′, 훽)) ∈ 퐸′

iff there is a timed transition from 〈푠, 훼〉

to 〈푠, 훼′〉 and a transition in

ꢂ

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

Fig. 1. Transitions in ꢃ and ꢃ′: 푎, 푏 ∈ Σ_푖, 푐 ∈ Σ_푖.

by a timed word from ℒ(ꢃ). If 훿(푎) = 0 for all

푎 ∈ Σ_푖, then the second condition for ꢀ is satisfied

trivially. Otherwise, Theorem 1 gives that this

condition is violated if and only if there is a

run

the complement 푅_푖of 푅_푖. The synchronized

product ℬ ×_Σℛ(ꢃ) recognizes the language

ꢂ

푅_푖||ℒ(ℛ(ꢃ))

({푤 | 푤|_Σ∈ 푅_푖∧ 푤|_Σ′∈

ꢂ

ℒ(ℛ(ꢃ))}). It follows Theorem 1 that

푅_푖||ℒ(ℛ(ꢃ)) = 푅_푖||푢푛푡ꢀ푚푒푑(ℒ(ꢃ)).

The

〈푠₀, [휈₀]〉 →^푒〈푠₁, [휈₁]〉 →^푒… →^푒〈푠_푚, [휈_푚]〉

in ℛ(ꢃ′) in which there are two transitions 푒_푙

and 푒_푙+ℎcorresponding to resetting clocks 푐_푖in

ꢃ′: 푒_푙= (〈푠_푙, [휈_푙]〉, 푎, 〈푠_푙+1, [휈_푙+1]〉 where 푎 ∈

푚

emptiness of the language generated by

ℬ × ℛ(ꢃ) is decidable in 풪(|ℛ × ℛ(ꢃ)|)

time. But 푅_푖||푢푛푡ꢀ푚푒푑(ℒ(ꢃ)) is empty if and

only if 푢푛푡ꢀ푚푒푑(ℒ(ꢃ))|_Σ⊆ 푅_푖. Hence, the

ꢂ

Σ_푖,

(〈푠_푙+ℎ, [휈_푙+ℎ]〉, 푏, 〈푠_푙+ℎ+1, [휈_푙+ℎ+1]〉 where 푏 ∈

Σ_푖, 휈_푙+ℎ+1(푐_푖) = 0, and transitions

휈_푙+1(푐_푖) = 0,

and

푒_푙+ℎ=

theorem is proved.

Now we consider the problem to decide if

all the strings generated by ꢃ satisfy the second

item of Definition 2. Let ꢃ = 〈퐿, 푠_퐼, Σ, 푋, 퐸, ℱ〉.

Let Σ_푖⊆ Σ. Let 푐_푖be a new clock variable,

푐_푖∈ 푋. Define ꢃ′ to be the automaton that is

the same as ꢃ except that transitions with label

in Σ_푖will have to reset the clock 푐_푖as well, i.e.

ꢃ′ = 〈퐿, 푠_퐼, Σ, 푋 ∪ {푐_푖}, 퐸′, ℱ〉, and 퐸′ = {푒′ =

(푠, 푎, 휙, 퐶 ∪ {푐_푖}, 푠′) | 푒 = (푠, 푎, 휙, 퐶, 푠′) ∈ 퐸 ∧

푎 ∈ Σ_푖} ∪ {푒′ = (푠, 푎, 휙, 퐶, 푠′) | 푒 =

푒_푙+1, … , 푒_푙+ℎ−1do not have label in Σ_푖(not

corresponding to transitions in ꢃ′ resetting

clock 푐_푖) that makes the following condition

satisfied: Let the run in ꢃ′ according to

Theorem 1 corresponding to that path be

푒

푙

푙+ℎ−1

〈푠_푙, 휈_푙〉 →_휏… →_휏

푙

푙+ℎ−1

〈푠_푙+ℎ, 휈_푙+ℎ〉 →^푒_휏〈푠_푙+ℎ+1, 휈_푙+ℎ+1

〉

푙+ℎ

Then, 휈_푙+ℎ(푐_푖) + 휏_푙+ℎ< 훿(푎). This implies the

following: After having removed all non-

reachable states from ℛ(ꢃ′), and adding time

transitions (labeled with “time”) to ℛ(ꢃ′), we

have that there is also a path in ℛ(ꢃ′)

(푠, 푎, 휙, 퐶, 푠′) ∈ 퐸 ∧ 푎 ∈ Σ_푖}We illustrate the

difference of transitions in ꢃ and ꢃ′ in Fig. 1.

Since clock variable 푐_푖does not appear in

any guard 휙 of ꢃ, the automaton ꢃ′ generates

the same timed language as ꢃ does. Adding the

clock variable 푐_푖is just for the purpose of

counting time between two (consecutive)

transitions in Σ_푖. A clock valuation for ꢃ′ now

is of the form 휈 ∪ {푐_푖↦ 푣} for some 푣 ∈

푅푒푎푙푠. Now we construct the region graph

ℛ(ꢃ′) for ꢃ′, and analyze this graph to see if

the second condition of Definition 2 is violated

푒

푙

푒

푙+ℎ−1

〈푠_푙, [휈_푙]〉 → … →

〈푠_푙+ℎ, [휈_푙+ℎ]〉 →^푡푖푚푒

〈푠_푙+ℎ, [휈_푙+ℎ+ 휏_푙+ℎ]〉 →^푒〈푠_푙+ℎ+1, [휈_푙+ℎ+1]〉

in which 휈_푙+ℎ(푐_푖) + 휏_푙+ℎ< 훿(푎) where 푎

is the label of 푒_푙, and 푒_푙+ℎhas label in Σ_푖. A

path in ℛ(ꢃ′) satisfying this condition is called

“violation” path. Now, checking for the

푙+ℎ

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

violation of the second condition of Definition

nonreachable states. Search in ℛ(ꢃ′) for a

single violation path. If such a path is found

for some i, stop with the output “no”.

2 from ꢃ is done by searching in the graph of

ℛ(ꢃ′) for a single path (not containing a loop)

from 푒_푙to 푒_푙+ℎwith the violation property as

mentioned above (we call it violation path). If

no such a path found, then the timed language

ℒ(ꢃ) satisfies the condition. This can be done

in 풪(|ℛ(ꢃ′)|²) time. Therefore, we have:

5. Stop with the output “yes”.

Note that a concurrent real-time system can

be modeled as a timed automata network which

is a synchronized product of a number of timed

automata, where the concurrency can be

expressed explicitly. A synchronized product of

a number of timed automata is also a timed

automaton, and hence, our algorithm works also

on timed automata networks.

Theorem 3 The problem “if a given timed

automaton

ꢃ

conforms to

real-time

concurrent interaction protocol 휋” is decidable

in time 풪(|ℛ(ꢃ′)|²).

We sumarizes our results in the following

deciding procedure:

Algorithm (Deciding if a timed automaton

satisfies a real-time interaction protocol)

Input:A real-time protocol 휋 =

4. Conclusion

We have proposed a simple but powerful

technique to specify interaction protocols for

the interface of components. Our model can

specify many aspects for interaction: the

temporal order between services, concurrency

for services, and timing constraints. We also

have shown that the problem of checking if a

timed automaton conforms to a given real-time

protocol is decidable, and developed a decision

procedure for solving the problem. The

complexity of the procedure is proportional to

the size of the region graph of the input timed

automaton which is acceptable for many cases

(like the way that the tool UPAAL handles

systems). We will incorporate this technique to

our model for real-time component-based

systems in our future work. We believe that our

results can be extended to the cases in which

systems are modeled by timed automata with

parameters, i.e. timed automata where a

parameter can appear in guards and can be reset

by a transition.

〈(Σ₁, 푅₁), … , (Σ_푘, 푅_푘), 훿〉,

푘

푖=1

where 훿:

Σ_푖→ ℕ^≥, and 푅_푖is a regular

⋃

expression on Σ_푖for ꢀ = 1, … , 푘.

A timed automaton ꢃ = 〈퐿, 푠_퐼, Σ, 푋, 퐸, ℱ〉 that

satisfies Σ_푖⊆ Σ for all ꢀ ≤ 푘.

Output: “Yes” if ℒ(ꢃ) ⊧ 휋, “no” otherwise.

Methods:

1. Construct the region automaton of ꢃ,

namely the automaton ℛ(ꢃ).

2. For each ꢀ = 1, … , 푘 construct automata

ℬ_푖that recognizes regular language 푅_푖.

Then, construct the synchronized product

ℛ(ꢃ) ×_Σℬ_푖and check if ℒ(ℛ(ꢃ) ×_Σℬ_푖)

ꢂ

is empty. If ℒ(ℛ(ꢃ) ×_Σ퐵_푖) is not empty

ꢂ

for some ꢀ, stop with output “no”.

3. If there is no time constraint in 휋, i.e. 훿 is

0 mapping on Σ, stop with output “yes”.

4. For each ꢀ = 1, … , 푘, where 훿 is not a 0-

mapping on Σ_푖, construct the timed

automaton

ꢃ′ = 〈L, s_I, Σ, X ∪ {c_i}, E′, ℱ〉, where E′ =

{e′ = (s, a, ϕ, C ∪ {c_i}, s′) | e =

Acknowledgments

(s, a, ϕ, C, s′) ∈ E ∧ a ∈ Σ_i} ∪ {e′ =

(s, a, ϕ, C, s′) | e = (s, a, ϕ, C, s′) ∈ E ∧

a ∈ Σ_i}, and then construct the region graph

ℛ(ꢃ′). Add all “time” transitions to ℛ(ꢃ′)

and simplify it by removing all

This research was funded by Vietnam

National Foundation for Science and

Technology Development (NAFOSTED) under

grant number 102.03-2014.23.

V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15

He on the Occasion of His 70th Birthday,

pages 136-150, 2013.

[5] Hung Ledang and Dang Van Hung. Timing

and concurrency specification in component-

References

[1] R. Alur and D.L. Dill. A Theory of Timed

Automata.

pages 183-235, 1994.

Theoretical Computer Science,

based

real-time

embedded

systems

[2] Luca de Alfaro and Thomas A. Henzinger.

Interface Automata. In ACM Symposium on

Foundation of Software Engineering (FSE), 2001.

[3] Jifeng He, Zhiming Liu, and Xiaoshan Li.

rCOS: A refinement calculus of object systems.

Theor. Comput. Sci., 365(1-2):109-142, 2006.

UNU-IIST TR 322.

development. In TASE, pages 293-304.

IEEE Computer Society, 2007.

[6] Stavros Tripakis, Ben Lickly, Thomas A.

Henzinger, and Edward A. Lee. On relational

interfaces.

EMSOFT’09, pages 67-76.

ACM, 2009.

[7] Dang Van Hung. Toward a formal model for

component interfaces for real-time systems. In

Proceedings of the 10th international workshop

on Formal methods for industrial critical

systems, FMICS ’05, pages 106-114, New York,

NY, USA, 2005. ACM.

[4] Dang Van Hung and Hoang Truong. Modeling

and specification of real-time interfaces with

UTP. In

Theories of Programming and

Formal Methods - Essays Dedicated to Jifeng

8 trang yennguyen 13/04/2022 6240

Download

Bạn đang xem tài liệu "A model for Real-time concurrent interaction protocols in component interfaces", để tải tài liệu gốc về máy hãy click vào nút Download ở trên

File đính kèm:

a_model_for_real_time_concurrent_interaction_protocols_in_co.pdf