Finite state automata as conceptual model for e-services

Integrated Design and Process Technology, IDPT-2003 Printed in the United States of America, June, 2003 c 2003 Society for Design and Process Science °

FINITE STATE AUTOMATA AS CONCEPTUAL MODEL FOR E-SERVICES Daniela BERARDI, Fabio DE ROSA, Luca DE SANTIS and Massimo MECELLA Dipartimento di Informatica e Sistemistica Universit`a di Roma “La Sapienza” via Salaria 113, I-00198 Roma, Italy E-mail: {berardi,derosa,lucads,mecella}@dis.uniroma1.it

ABSTRACT Recently, a plethora of languages for modeling and specifying different facets of e-Services have been proposed, and some of them provides constructs for representing time. Time is needed in many contexts to correctly capture the dynamics of transactions and of composability between e-Services. However, to the best of our knowledge, all the proposed languages for representing e-Service behaviour and temporal constraints lack both a clear semantics and an underlying conceptual model. In this paper, we propose a conceptual representation of e-Service behaviour, taking time constraints into account, and a new XML-based language, namely WSTL (W EB S ERVICE T RANSITION L ANGUAGE), that integrates well with standard languages in order to completely specify e-Services. In particular, WSTL allows for specifying an e-Service starting from its conceptual representation, in a straightforward way. INTRODUCTION Since the last few years, we are witnessing a great change in business paradigms. Different companies are able to pool together their services, in order to offer more complex, value added products and services. Thanks to the spreading of network technologies and the Internet, that makes services easily accessible to a vast number of customers, companies are able to cooperate in very flexible ways, giving rise to the so called virtual enterprises [Georgakopoulos, 1999]. Although it started in the business context, the scenario of interorganization cooperation has spread out different contexts, e.g., e-Government [Elmagarmid and McIver Jr, 2001]. Inter-organization cooperation can be supported by Cooperative Information Systems (CIS’s) [De Michelis et al., 1997]. Many approaches have been proposed for the design and development of CIS’s: business process coordination and service-based systems [Dayal et al., 2001], agentbased technologies and systems [Castro et al., 2002], schema and data integration techniques [Rahm and Bernstein, 2001], [Lenzerini, 2002]. In particular, the former approach focuses on cooperation among different organizations that export services as semantically defined functionalities; cooperation is achieved by composing and integrating services over the Web. Such services, usually referred to as e-Services or Web

Services, are available to users or other applications and allow them to gather data or to perform some tasks. In the following, we will refer to Service Oriented Computing (SOC) as a new emerging model for distributed computing that enables to build agile networks of collaborating business applications distributed within and across organizational boundaries 1 . Cooperation of e-Services poses many interesting challenges regarding, in particular, composability, synchronization, coordination, correctness verification [Yang et al., 2002]. Indeed, in order to address such issues in an effective and correct way, the dynamic behaviour of e-Services needs to be formally represented. There have been some preliminary efforts in this direction: [Mecella et al., 2001] defines the notion of compatibility and dynamic substitition of e-Services, [Kuno et al., 2001], [BEA et al., 2002] propose standards to describe the interfaces and the conversations of e-Services. Recently, some research efforts are concerned with adding a fundamental concept: time. Time is needed in many contexts to correctly capture the dynamics of transactions and of composability. Many e-Services available on the Internet are made up of sessions having an associated time-out, as those that allow a user to check his bank account, or to participate to an online auction. Analogously, we often face trade-offs involving time: when we want a fast high quality service, but no e-Service has both these features, we have to choose between speed and quality. In this paper we propose a conceptual representation of e-Service behaviour that takes time into account, and introduce an XML-based language, that can be integrated with standard languages in order to completely specify e-Services. In particular, the proposed language allows for specifying an e-Service starting from its conceptual representation, in a straightforward way. LANGUAGES FOR E-SERVICES Recently, a plethora of languages for modelling and specifying different facets of service oriented computing have been proposed; in this section, we discuss some of them, with respect to the concept of Service Oriented Architecture (SOA) [HP, 2001], in order to correctly compare all such 1 The

Service Oriented Computing net: http://www.eusoc.net

2 ' ! "  -  ! " #   -+ ) -4 # 3 "%! 55" 6# "(4 30" & /8 3 & 0 '  " "/-5 6 92  #% ) 3 " 3 % 5 & "6 7 "+' )) 0 -; " ): & 0 /  ! " # /- "  # & ' 9          
  

  


  
    


<   = > ? @ A  F GN HO IP JQ K R L S G M B  C  = D 

Fig. 1.

 $ %  ! " & #' (" ) ! ' *   , " ) -! "" )# ./ (& 0 + , 1 & 

E    = D  
  

 
 

Service Oriented Architecture

works. The aim is to show that a conceptual way of representing e-Services is still lacking, and this constitutes the motivation of our work. A SOA is the minimal framework for e-Services consisting of some basic operations and roles (see Figure 1): – Service Provider: it is the subject providing software applications for specific needs as services; (i) from a business perspective, this is the owner of the service (e.g., the subject which is possibly paid for its services), and (ii) from the architectural perspective, this is the platform the service is deployed onto. Available services are described by using a service description language and advertised through the publish() operation on a public available service directory. – Service Requestor: it is the party that uses the services; (i) from a business perspective, this is the business requiring certain services to be fulfilled (e.g., the payer subject), and (ii) from an architectural perspective, this is the application invoking the service. A service requestor discovers the most suitable service in the directory through the find() operation, then it connects to the specific service provider through the bind() operation and finally it uses the chosen service (invoke() operation). – Service Directory: it is the party providing a repository and/or a registry of service descriptions, where providers publish their services and requestors find services. The transport medium is a parameter of a SOA, therefore such a framework is easily integrable on different technologies; specifically, an e-Service Architecture is one in which the transport medium is electronic, whereas in a Web Service Architecture the transport medium is the Web. All emerging proposals consider the last scenario, in which services “live” over the Web, on the basis of a common transport medium, consisting of Web technologies such as HTTP, SOAP and XML Protocol [W3C, 2002]. They address some basic technological issues of a SOA, that is the definition (i) of the service directory, (ii) of the service description language,

(iii) of possible interactions a service can be involved in (i.e., the conversations), and (iv) of how to compose and coordinate different services, to be assembled together in order to support complex processes (i.e., the orchestration). In the UDDI initiative, the architecture of a distributed service directory is proposed [UDDI.org, 2001]. In the context of the W3C, many service description languages are being proposed for specific purposes: Service Description Language – Web (WSDL, [Ariba et al., 2001]) for describing services, specifically their static interfaces; – Web Service Conversation Language (WSCL, [Kuno et al., 2001]) for describing the conversations a service supports; the underlying model is the one of the activity diagrams; – Web Service Choreography Interface (WSCI, [BEA et al., 2002]) for describing the observable behavior of a service in terms of temporal and logical dependencies among the exchanged messages; – Web Service Flow Language (WSFL, [Leymann, 2001]) for the design of composite Web Services starting from simple ones (composition of Web Services); the underlying model is the one of Petri Nets; – XLANG [Satish, 2001] for both the specification of the behavior of services and their orchestration; in [Meredith, 2002], it has been pointed out that this language is complete, it owns the property of composability and that the underlying theoretical model is the one of process algebra; – Business Process Execution Language for Web Services (BPEL4WS, [Curbera et al., 2002]) with the aim of merging WSFL and XLANG. With respect to the SOA, the languages WSDL, WSCL and WSCI concerns the service provider, and are all service description languages: WSDL addresses only static interface specifications, whereas WSCL and WSCI considers also behavioral issues and time. More in details, WSDL, analogously to an interface definition language (e.g., CORBA IDL), describes methods, ingoing and outgoing messages and data types used by the service. Moreover, it supplies a mechanism to locate the service (e.g., using a URI), the protocol used to exchange messages and the concrete mapping between the abstract method definition and the real protocol and data format. WSDL define what the e-Service does, not how it does it; moreover WSDL does not express the semantics of message exchange neither their correct order. WSCL models the conversation (sequence of exchanged messages) supported by an e-Service: it specifies the XML documents being exchanged, and the allowed sequence, in a fashion similar to an activity diagram. A WSCL document is composed of four main elements: (i) document type descriptions specifying the types (schemas) of XML documents the service can accept and send during the conversation, (ii) interactions modelling the actions of the conversation as document exchanges between two participants (i.e., the e-Service and

its client), (iii) transitions specifying the order relationships between interactions, and (iv) conversations, listing all the interactions and transitions that make up the conversation. WSCI can be considered as a evolution of WSCL: it describes the observable behavior of an e-Service and how operations can be choreographed in the context of message exchanges in which the e-Service participates. WSCI allows to describe the correct order of the exchanged messages and permits to define multiple behaviors for the same e-Service on the basis of the context in which is used. Furthermore, it provides methods to manage exceptional situations, such as timeouts and fault messages 2 . WSCI, finally, allows to define the abstract behavior of a process that involves more e-Services in term of interfaces and links between operations, thus giving a view of the process in terms of message exchanges; with such a respect, WSCI is also an orchestration language. As far as the languages WSFL, XLANG and BPEL4WS, they are orchestration and coordination languages, aimed at specifying how multiple e-Services are coordinated and the state and the logic needed for such a coordination; they provide constructs for limited time modelling, for correlation of e-Service instances and for exception management. Orchestration languages will be not further addressed in this paper. C ONCEPTUAL R EPRESENTATION OF e-S ERVICES From the previous discussion, it stems that some proposals address the issue of service behavior representation, considering also time; but we argue that (i) a clear semantics of such languages is missing, and (ii) they are not suitable for service oriented computing design at a conceptual level. We argue that in service oriented computing we need conceptual languages in order to represent e-Services from an external point of view; such external point of view is the one to be considered when composing and orchestrating services. Moreover we need also languages for internal specification, i.e., specifying the e-Service for designers and implementors. In this work we concentrate only on the former issue (i,.e., external conceptual representation), since, for the latter purpose, classic specification languages used in software engineering practice can be used. We propose a conceptual way of representing e-Service behavior, including time, based on finite state automata, and a new language, namely WSTL 3 (W EB S ERVICE T RANSITION L ANGUAGE ), that can be used to represent an e-Service specification at a “technological” level, obtained by a straightforward mapping from the e-Service specification at a conceptual level 4 . In this way, we are able to give a clear and formal semantics to WSTL constructs. WSTL integrates well with other languages: e-Service specifications, which are expressed in WSTL and stored into suitable registries/repositories, complement standard WSDL specifications. 2 Time modelling is delegated to the delay element for represent time interval and to the onTimeout event handler for timeout situations. 3 The XML Schema is available at http://www.dis.uniroma1.it/ ∼mecella/projects/vispo/WSTL/WSTL1.1.xsd 4 Note that the conceptual specification is independent from any technology.

Figure 2 shows the proposed conceptual approach: a cooperative designer, which is interested in searching, reusing, composing, and orchestrating e-Services (which are all based on e-Service external facets), defines an e-Service conceptual specification. Such a specification is then translated into a technological, i.e., based on standard XML-based languages, representation; such a representation consists both of a WSDL file that specifies the static interface of the e-Service, and of a WSTL file, representing the e-Service behavior. Such files are then published into service directories, and then used for future searches, compositions, orchestrations, etc. Starting from the e-Service conceptual specification, internal designers and implementers will produce software artifacts implementing the e-Service. An initiative which is quite similar to the proposed conceptual approach is the one of the DAML-S Coalition [Ankolekar et al., 2002]. DAML-S is an ontology for describing Web Services that enables the definition of service content vocabulary in terms of objects and complex relationships between them, including class, subclass relations, cardinality restrictions, etc., including all XML typing information. More in details, the DAML-S Ontology comprises: – ServiceProfile. This is like the yellow page entry for a service. It relates and builds upon the type of content in UDDI, describing properties of a service necessary for automatic discovery, such as what the services offers, and its inputs, outputs, and its side-effects (preconditions and effects). – ServiceModel. Describes the service’s process model (the control flow and data-flow involved in using the service). It is designed to enable automated composition and execution of services. – ServiceGrounding. Connects the process model description to communcation-level protocols and message descriptions in WSDL. The part of DAML-S more related to our work is the process model; its semantics has been defined both through a translation to (axiomatization in) first-order logic, and through a translation to an operational semantics using Petri Nets. WSTL WSTL is a XML-based description language able to represent the observable behavior of e-Services. WSTL does not address the implementation that actually drives the interactions; rather, it allows to describe what is observable from the point of view of the service users. Although simple, it permits to model complex behaviors, such as loops and exceptions. WSTL extends the static interface of WSDL with elements which describe the correct sequence of the exchanged messages. The root element of WSTL is the Conversation construct 5 ; it describes the acceptable interactions of the eService in a message exchange scenario. Each WSTL con5 The “?” symbols associated to an element means that the element can occur zero or one time; the “+” symbol states that the elements must occur at least once.

Cooperative Designer design of external e-Service specification

e-Service Conceptual Specification (based on Finite State Automata)

search into

Service Directory

translation

store for advertising, search, use, composition, etc.

WSDL File

refinement for e-Service implementation (internal specification)

WSTL File

Software Artifact implementing e-Service

e-Service Technological Representation (based on Web Service / XML Languages)

Fig. 2.

Conceptual approach to e-Service specification

versation is characterized by a name and it can contain one or more Transition elements. ; however, by adopting a black box approach, we skip over internal computations and represent only the input/output behavior of e-Service from the client view point, i.e., that have some effects towards the client: each interaction is therefore described by the pair < input command, output message > only. At a given point, the input command that can be sent to the e-Service depends on the previous ones, and the client chooses the next command on the basis of the information returned by the previous output messages. At least in principle, interactions between an e-Service and its client may be unlimited, as in the case of an e-Service offering a continuous service, e.g., periodically delivering a product. According to these considerations, an e-Service can be fully modelled as an execution tree [Berardi et al., 2003], whose branches represent all possible sequence of interactions between an eService and its client. However, since execution trees do not have a finite representation, we decide to resort to classes of e-Services that can be captured in a finite way. We propose to represent an e-Service as a Finite State Automaton (FSA), since Finite State Automata (FSA’s) are a widely known, simple but powerful formalism, that allow us to capture a large class of e-Services. FSA’s allow to model the behavior of a system as a sequence of transitions: in this way, we focus on the operational semantics of e-Services, i.e., we

represent how they evolve and with which results, according to which command is invoked. In particular, we consider each e-Service interaction as a state transition, labeled with the pair < input command, output message >, where each state represents the history of executed sequence of interactions between the client and the e-Service. Let eS be an e-Service. Its representation as FSA is a tuple of the form S = < I, O, Γ, s0 , F, δ >, where: – I is a non empty set of input commands, and O is a non empty set of output messages; I × O is the alphabet of the FSA; – Γ is a finite, non empty set of states; – s0 ∈ Γ is the initial state; – F ⊆ Γ is a non empty set of final states, i.e., states where the client can terminate its interaction with the e-Service; – δ : Γ × I × O → Γ is the transition function, that represents the evolution of the FSA from a state to another one, for a given pair < input command, output message > 6 ; the transition function can be undefined on the final states. We assume that s0 ∈ F , since a client may decide not to start the execution of an e-Service, even if he instantiated the e-Service. Indeed, an e-Service need to be instantiated before it can be invoked, and its execution starts when the first input command is given [Mecella and Pernici, 2002]. A configuration is a pair < s, i, o >, where s ∈ Γ, i ∈ I and o ∈ O. An execution of an e-Service is a finite, non empty sequence of configurations < s0 , i0 , o0 >, . . . , < sj , ij , oj >, < sj+1 , ij+1 , oj+1 >, . . . , < sn , in , on >, where s0 is the initial state, sn is a final state, i.e., sn ∈ F, and such that δ(sj , ij , oj ) = sj+1 . The set of all executions forms the behavior of the e-Service. Example 1: Let S1 be an e-Service that allows a client to sell and to buy stocks online (see Figure 3). After instantiating the e-Service, the client inserts its userID and password (input command userData): the e-Service validates the client and check the maximum amount that can be spent. This information is displayed to the client (output message checkedAccount). If, conversely, the client does not provide valid credentials, the e-Service will output a different output message notValidClient, thus terminating its interaction with the client. After visioning its available amount, the client invokes the continue command, in order to proceed to the stock trading; data on stocks are displayed (message displayedStockData) and the client can decide to sell (command sell) or buy (command buy) stocks: after each of these commands, information on the task result is displayed (message displayedResults). Finally, the client can decide to stop performing stock exchange transactions 6 State transitions are deterministic, since given a state, an input command and its corresponding output message, the successor state is univocally identified.

buy/displayedResults userData/checkedAccount

s0

continue/displayedStockData

s1

s2

s3 stop/emailNotification

userData/notValidClient

sell/displayedResults

s4 Fig. 3.

“Trading stocks” e-Service

(command stop) and he is notified with an e-mail about his transactions (message emailNotification). This e-Service allows for many different executions, as for example: – userData/checkedAccount, continue/displayedStockData, sell/displayedResults, buy/displayedResults, stop/emailNotification, in which a client operates a stock sale followed by a stock purchase; – userData/checkedAccount, continue/displayedStockData, stop/emailNotification, in which the client uses the e-Service without any trading; – userData/notValidClient, in which the client provides not valid credentials. The client can terminate the interaction with the e-Service only in the two final states s3 and s4 . ¤ Usually, e-Services similar to the one of Example 1, have additional behavior: in some scenarios, just to provide an example, when an e-Service has not received any command from the client within a given instant, because of network overloading or because the client has exceeded the time limit for invoking the command, an error message is output to the client. In order to capture also such situations, absence of input commands or of output messages, as well as time constraints, need to be captured. We introduce a new symbol ², that represents the lack of an input command or the absence of an output message: we refer to ² as the empty input command/output message. Note that an empty input command does not imply absence of internal computations (and therefore of the possible output message), since it may be the case that a computation starts with no triggering command, and it correctly returns an output message. We do not allow for the pair ²/², since no semantics can be associated to it from a user point of view. Analogously, each execution of an e-Service consists of at least one nonempty input command or one non-empty output message, otherwise no semantics can be associated to an execution. An e-Service with time constraints on transitions can be modelled by using Timed Finite State Automata (TFSA’s). TFSA’s have been discussed in many papers, e.g., [Henzinger et al., 1994], [Alur and Dill, 1994]: starting from

the discussion in these papers, we will slightly modify the previous definition in order to cope with time. We make each transition depending also on the instants when the input command and the output message are invoked and returned, respectively. Additionally, we add two timing functions τ and σ: the former associates an input command with the duration of time within which this command needs to be executed by the client; the latter associates an output message with the duration of time within which the task triggered by the input command needs to be completed and the output message has to be returned by the e-Service; duration are considered starting from the instant in which the current state is entered. We assume that each e-Service has its own timing functions. Let eS T be a timed e-Service. Its representation as TFSA is a tuple of the form S T =< I, O, Γ, ², s0 , F, T , δ, τ, σ >, where: – I, O, Γ, s0 , F are defined as in the previous definition; – T is the set of timings, denoted by non negative integers; – ² denotes both the empty input command and the empty output message; – τ : Γ × I → T is the starting timing function, that defines the maximal duration of time by which an input command should be given in a specific state; – σ : Γ × O → T is the ending timing function, that computes the maximal duration of time by which a computation is executed and the output message is returned, for a given state and a given output message. In particular, • on the final states having no outgoing transition, τ and σ are undefined; • on the initial state, τ and σ are defined wrt the instant when the e-Service is instantiated 7 . Note that since τ and σ impose timing constraints transition by transition, we can choose not to impose any constraint on a transition. Additionally, τ and σ are undefined on ², since it makes no sense defining a time constraint in a situation where either the input command or the output message is absent. – δ : Γ × [((I ∪ {²}) × (O ∪ {²})) − ({²} × {²})] × T × T → Γ is the transition function. In particular, within the 7 We recall that an e-Service needs to be instantiated before it can be invoked [Mecella and Pernici, 2002].

γ/α

²/β

s1

s2

s3

(a) Case 1 α/β s1 α/² s1

²/γ

β/γ s2

s3

s3

(b) Case 2 α/² s1

s2

(c) Case 3

²/β s2

s3 α/β s1

s2 γ/²

s1

α/β

s3

(d) Case 4

Fig. 4.

s3

(e) Case 5

Analysis of possible cases in which ² labels a timed transition

expression δ(sj , i, o, ti , to ), ti and to have the following meaning: • if both i and o are different from ², then the to is the instant at which the output message o has been returned, ti is the instant at which the input command i has been invoked, • if i (resp. o) is ², we set ti = to , and ti (resp. to ) is intended as above. Finally, note that the transition function can be undefined on the final states. The notions of configuration, execution and behaviour of an e-Service can be straightforwardly obtained from the analogous definitions previously given. In order to correctly capture timing on e-Services, several natural properties must be satisfied. In the following, we discuss them and we show how they can be imposed on δ, τ and σ: 1) each transition cannot terminate before it has started, i.e., each output message cannot be returned before the corresponding input command; 2) each transition cannot start before the previous one has completed, i.e., each input command cannot be given before the previous output message has been returned (if the latter exists); 3) as far as δ is concerned, each input command and output message within each transition must be returned within the expected interval (when defined). Noting that Property 2 is naturally captured by the definition of transition function, the other properties can be encoded in δ as follows: ∀sj , sj+1 , i, o, ti , to : δ(sj , i, o, ti , to ) = sj+1 if

ti ≤ to ∧ ti ≤ τ (sj , i) ∧ to ≤ σ(sj , o). If either i or o are empty, or in general if τ and σ are not defined, this expression simplify straightforwardly. As far as τ and σ are concerned, Property 1 can be imposed as ∀s∀i τ (s, i) ≤ σ(s, o). Property 2 is guaranteed from the fact that both τ and σ are defined wrt the current state, transition by transition. However, this holds when both the input command and the output message are not empty. If either one of them is ², several cases may happen, as shown in Figure 4, where α and β denote input message or output message that are different from ², whereas γ can denote also ² (when admissible). As far as cases 1 and 2 are concerned, Property 1 is meaningless, since no timing constraints can be imposed on ². In the situation shown in Figure 4(c), Properties 1 and 2 express the fact that β cannot be returned before α is invoked: this is captured by τ (s1 , α) < σ(s1 , β). Situation in the upper part of Figure 4(d) needs to be reduced to the situation in the lower part, in which ² is not present. As far as the case 5 is concerned, the presence of ² does not influence the choice of which transition is to be taken, since the timing constraints imposed by τ on the input commands determine the choice. In cases like this we assume that τ (s1 , α) is greater (or less) than τ (s1 , γ): this implies that γ is different from α. The same applies for σ and the output messages. The proposed formalization naturally allows for capturing additional time constraints, as those imposing that the interval between the instant when an input command is invoked and the instant when the corresponding output message is returned is less than a given duration. Note that such timing constraints can be imposed independently from the fact that τ and σ are defined within a transition or not. Before concluding the section, we apply our formalization to an example. Example 2: Figure 5 shows the e-Service discussed in Example 1, extended with time constraints and ² transitions. In particular, this e-Service has the following behaviour: – if the command userData is not given within the expected interval, the output message failed is returned; – if the output message displayedResult associated to command buy is not returned before a given time, the message setStopAndNotify is returned, that stops the stock trading, notifies the client about this problem and reports to him about the stocks trade. The same happens for output message displayedResult associated to command sell; Additionally, we impose several temporal constraints on transitions, defined by τ and σ, as shown in Figure 6. The transition function δ is also defined in Figure 6. The constraints on τ and σ are: τ (s0 , userData) ≤ σ(s0 , checkedAccount) τ (s0 , userData) ≤ σ(s0 , f ailed) τ (s0 , userData) ≤ σ(s0 , notV alidClient) ¤ MAPPING The FSA model of e-Services introduced in previous section gives us the possibility to exploit the results obtained in the

s4

buy/setStopAndNotify

²/failed

buy/displayedResults continue/displayedStockData

s0

s1

s2

stop/emailNotification

s6

s3

userData/checkedAccount sell/displayedResults sell/setStopAndNotify

userData/notValidClient

s7

s5 Fig. 5.

δ(s0 , userData, checkedAccount, ti1 , to1 ) = s1 δ(s0 , ², f ailed, to2 , to2 ) = s4 δ(s0 , userData, notV alidClient, ti1 , to3 ) = s5 δ(s1 , continue, displayedStockData, ti4 , to4 ) = s2 δ(s2 , buy, displayedResults, ti5 , to5 ) = s2 δ(s2 , buy, setStopAndN otif y, ti5 , to6 ) = s6 δ(s2 , sell, displayedResults, ti7 , to7 ) = s2 δ(s2 , sell, setStopAndN otif y, ti7 , to8 ) = s7 δ(s2 , stop, emailN otif ication, ti9 , to9 ) = s3 Fig. 6.

“Trading stocks” timed e-Service

if if if if if if if if if

ti1 to2 ti1 ti4 ti5 ti5 ti7 ti7 ti9

≤ to1 ∧ ti1 ≤ τ (s0 , userData) ∧ to1 ≤ σ(s0 , checkedAccount) ≤ σ(s0 , f ailed) ≤ to3 ∧ ti1 ≤ τ (s0 , userData) ∧ to3 ≤ σ(s0 , notV alidClient) ≤ to4 ≤ to5 ∧ to5 ≤ σ(s2 , displayedResults) + ti5 ≤ to6 ≤ to7 ∧ to7 ≤ σ(s2 , displayedResults) + ti7 ≤ to8 ≤ to9

Transition function for “trading stock” e-Service

literature about FSA’s in order to prove important properties, such as the correctness of an e-Service, wrt its intended behavior, in order to remove unexpected behaviors. This opportunity, however, would be useless without techniques for translating this abstract model into a concrete, standardcompliant representation. In this section we aim at illustrating how to obtain the specification of an e-Service in WSTL, starting from its conceptual representation as a FSA. In what follows, we illustrate the rules used to map a FSA into a WSTL document. The complete e-Service specification is then constituted by such a WSTL document plus a WSDL document containing message type definitions. First, we associate a WSDL message type with each input command and with each output message. For example, for the input command ij , we obtain the following message: