Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadata
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Wednesday, May 13, 2015 - 4:37:29 PM
Last modification on : Friday, February 4, 2022 - 3:34:02 AM
Long-term archiving on: : Wednesday, April 19, 2017 - 7:09:02 PM


Files produced by the author(s)




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



Record views


Files downloads