Output details
11 - Computer Science and Informatics
Middlesex University
A Framework for Reasoning on Component Composition
<10> This paper presents the formalisation in Isabelle/HOL of the Grid Component Model (GCM), an industrial component standard introduced by Inria and French Telecom and used in the Inria spin-off ActiveEON. It is the first time that GCM has been formalized in an interactive theorem prover. The 2009 FMCO conference has seen our reduction semantics model for GCM, part of Marcela Rivera's PhD. Isabelle/HOL allows capturing this semantics of asynchronous invocations and component synchronisation. The paper is an important part of the PhD of Muhammad Uzair Kahn now an Assistant Professor at National University of Computer and Emerging Sciences in Islamabad.