Review: Formal Methods for Open Object-Based Distributed Systems VReport as inadecuate

Review: Formal Methods for Open Object-Based Distributed Systems V - Download this document for free, or read online. Document in PDF available to download.

1 MIRHO - Objects, types and prototypes : semantics and validation CRISAM - Inria Sophia Antipolis - Méditerranée , UHP - Université Henri Poincaré - Nancy 1, Université Nancy 2, INPL - Institut National Polytechnique de Lorraine, CNRS - Centre National de la Recherche Scientifique : UMR7503 2 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems CRISAM - Inria Sophia Antipolis - Méditerranée

Abstract : Distributed System V FMOODS is not a book. It is a luxurious conference proceeding, edited in 2002 under the -shield- of IFIP TC6-WG6.1. FMOODS conference bring researchers from various fields: formal methods model checking, abstract interpretation, type theory, Hoare-logic, etc., distributed systems CSP, pi-calculus, ambients, petri nets, actors, agents, ORB-s, etc., and -all around- object-based theory and practice. Applications in the above fields are various, crucial and pragmatic. Just to mention a few of these: hardware design, security and communication protocols, distributed-embedded-concurrent-collaborative systems, Java software verification, middleware, interoperability, computer-aided collaborative work, air traffic control, telephony features, etc. We think that the community of researchers involved in developing those applications is now mature to use formal methods and proof assistants to design-develops-certify -safe software- in the above -hot fields-. The major cost in the design phase it is well understood that a fairly concrete mathematical model costs more in terms of human resources than a UML chart will benefit from a major -solidity- of the specification of the related software; in latest experiments using certain proof assistants, proofs of the soundness of the specifications can be turned directly into executable code. We are of course far from a -democratization- of such techniques which can actually be used only by experts but their recent use in the setting of formal certification of critical applications such as smart-card, embedded software, compilers, protocols for cryptography, Java language, etc., shows that in the near future their use might be as widespread as the use of C++ libraries, or design patterns, or object-orientation. A few drawbacks: the rate of submitted-accepted papers is not known, and only one of the three invited presentations have produced a regular paper the others ones only gives abstracts. Moreover, technical papers should have been more expanded extended versions of some of them can be found on the web. Due to the very high price of the volume 111 GBP, a collection of the long versions of the best papers would have been a more appropriate and seducing post-conference proceeding. The volume is suitable and of interest for the intended audience, that is researchers in those fields.

Keywords : formal methods object-oriented distributed systems

Author: Luigi Liquori -



Related documents