seminar Tomase Barrose 26. a 27.10.

[Vladimir Mencl]

Dobry den,

v ramci sve navstevy v Praze prednese na seminari dva prispevky
Tomás Barros (INRIA, France).

Termin techto seminaru je 26.10. a 27.10. v obvyklou hodinu.

Puvodne naplanovane seminare P. Jezka a J. Kofrone jsou o tyden
odlozeny.

Aktualni program seminare je k dispozici na
http://nenya.ms.mff.cuni.cz/teaching/seminar.phtml

Tesim se na vasi ucast
Vladimir Mencl

------------------------------------------------------------

* 10/26/04, 14:00
    Tomás Barros (INRIA, France): Parameterized Models for Distributed
	Java Objects

  Distributed Java applications use remote method invocation as a
communication means between distributed objects. The ProActive
library provides high level primitives and strong semantic guarantees
for programming Java applications with distributed, mobile, secured
components. We present a method for building finite, parameterized models
capturing the behavioural semantics of ProActive objects. Our models are
symbolic networks of labelled transition systems, whose labels represent
(abstractions of) remote method calls. In contrast to the usual finite
models, they encode naturally and finitely a large class of distributed
object-oriented applications. Their finite instantiations can be used in
classical model-checkers and equivalence-checkers for checking temporal
logic properties in a compositional manner. We are building a software
tool set for the analysis of ProActive applications using these methods.

* 10/27/04, 9:00
    Tomás Barros (INRIA, France): Parameterized Specification
	and Verification of the Chilean Electronic Invoices System

  We present the complete process of a formal specification and
verification of the Chilean electronic invoice system which has been
defined by the tax agency. We use this case study as a real-world and
real-size example to illustrate our methodology for specification and
verification of distributed applications. Our approach is based on a new
hierarchical and parameterized model for synchronised networks of labelled
transition systems. In this case study, we use a subset of the model as
a graphical specification language. We check this formal specification of
the invoice system against its informal requirements, described in terms
of parameterized temporal logic formulas. Their satisfiability cannot be
checked directly on the parameterized model: we introduce a method and a
tool to instantiate the parameterized models and properties, allowing to
use standard (finite-state, bisimulation-based) model-checkers for the
verification. We also illustrate the use of different methods to avoid
the state explosion problem by taking advantage of the parameterized
structure and instantiations.