Review: Formal Methods for Open Object-Based Distributed Systems V

Luigi Liquori 1, 2
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
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.
Type de document :
Article dans une revue
The Computer Journal, Oxford University Press (UK), 2003, 46 (6), pp.661. 〈Oxford University Press on behalf of British Computer Society.〉. 〈10.1093/comjnl/46.6.661〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01149616
Contributeur : Luigi Liquori <>
Soumis le : mercredi 13 mai 2015 - 16:37:29
Dernière modification le : vendredi 12 janvier 2018 - 01:48:42
Document(s) archivé(s) le : mercredi 19 avril 2017 - 19:09:02

Fichier

2003-tcj-book-review.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Luigi Liquori. Review: Formal Methods for Open Object-Based Distributed Systems V. The Computer Journal, Oxford University Press (UK), 2003, 46 (6), pp.661. 〈Oxford University Press on behalf of British Computer Society.〉. 〈10.1093/comjnl/46.6.661〉. 〈hal-01149616〉

Partager

Métriques

Consultations de la notice

244

Téléchargements de fichiers

54