Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: timed automata with discrete data

Sortuj według:

Ogranicz wyniki do:

Towards Automatic Composition of Web Services : SAT-Based Concretisation of Abstract Scenarios

Niewiadomski A., Penczek W., Półrola A., Szreter M., Zbrzezny A.

Fundamenta Informaticae

2012

Vol. 120, nr 2

181-203

Automating the composition of web services is an object of a growing interest. In our paper [13] we proposed a method for converting the problem of the composition to the problem of building a graph of worlds consisting of formally defined objects, and presented the first phase of this composition aimed at building a graph of types of services (an abstract graph). In this work we propose a method of replacing abstract flows of this graph by sequences of concrete services able to satisfy the user’s request. The method is based on SAT-based reachability checking for (timed) automata with discrete data and parametric assignments.

Runtime Monitoring of Contract Regulated Web Services

Lomuscio A., Penczek W., Solanki M., Szreter M.

Fundamenta Informaticae

2011

Vol. 111, nr 3

339-353

We investigate the problem of locally monitoring contract regulated behaviours in agentbased web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfillment (or violation) of contractual obligations. A key feature of the framework is that it is fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by multiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.

Towards verification of Java programs in VerICS

Orzechowski M., Woźna B., Siwiak T.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2006

Nr 997

1-33

VerICS has been designed as a tool for automated verification of timed automata, and protocols written in both Intermediate Language and a specification language Estelle. Recently, the tool has been extended to work with so called Timed Automata with Discrete Data and multi-agent systems. The paper presents a prototype of a translator from a subset of the Java programming language to Intermediate Language and Time Automata with Discrete Data, the modeling languages of the VerICS model checker.

Verics został zaprojektowany jako narzędzie do automatycznej weryfikacji automatów czasowych oraz protokołów zapisanych zarówno w języku pośrednim jaki i języku Estelle. Ostatnimi czasy Verics został rozbudowany i obecnie pozwala również na automatyczną weryfikację systemów wieloagentowych oraz protokołów zapisanych za pomocą formalizmu rozszerzonych automatów czasowych. Praca ta opisuje translator z pewnego podzbioru Javy, popularnego ostatnio języka programistycznego, do rozszerzonych automatów czasowych i do języka pośredniego, formalizmów będących językami wejściowymi dla werifikatora Verics.