Institutional Research Information Service
UCL Logo
Please report any queries concerning the funding data grouped in the sections named "Externally Awarded" or "Internally Disbursed" (shown on the profile page) to your Research Finance Administrator. Your can find your Research Finance Administrator at https://www.ucl.ac.uk/finance/research/rs-contacts.php by entering your department
Please report any queries concerning the student data shown on the profile page to:

Email: portico-services@ucl.ac.uk

Help Desk: http://www.ucl.ac.uk/ras/portico/helpdesk
Publication Detail
Validating distributed object and component designs
  • Publication Type:
  • Authors:
    Kaveh N, Emmerich W
  • Publisher:
    Springer Verlag
  • Publication date:
  • Pagination:
    63, 91
  • Chapter number:
    Vol. 2804
  • Series:
    Lecture Notes in Computer Science
  • Editors:
    Bernardo M,Inverardi P
  • ISBN-10:
  • Book title:
    Formal Methods for Software Architectures: Third International School on Formal Methods for the Design of Computer, Communication and Software Systems: Software Architectures, SFM 2003, Bertinoro, Italy, September 22-27, 2003
  • Notes:
    Imported via OAI, 7:29:01 3rd Aug 2005
Distributed systems are increasingly built using distributed object or component middleware. The dynamic behaviour of those distributed systems is influenced by the particular combination of middleware synchronisation and threading primitives used for communication amongst distributed objects. A designer may accidentally choose combinations that cause a distributed application to enter undesirable states or violate liveness properties. We exploit the fact that modern object and component middleware offer only a small number of underlying synchronisation primitives and threading policies. For each of these we define a UML stereotype and a formal process algebra specification of the stereotype semantics. We devise a means to specify safety and liveness properties in UML and again map those to process algebra safety and liveness properties. We can thus apply model checking techniques to verify that a given design does indeed meet the desired properties. We propose how to reduce the state space that needs to be model checked by exploiting middleware characteristics. We finally show how model checking results can be related back to the input UML models. In this way we can hide the formalism and the model checking process entirely from UML designers, which we regard as critical for the industrial exploitation of this research.
Publication data is maintained in RPS. Visit https://rps.ucl.ac.uk
 More search options
UCL Researchers
Dept of Computer Science
University College London - Gower Street - London - WC1E 6BT Tel:+44 (0)20 7679 2000

© UCL 1999–2011

Search by