Harnessing rCOS for Tool Support—The CoCoME Experience - Formal Methods and Hybrid Real-Time Systems - page 112

We have analyzed the software development process in a commercially suc-
cessful tool (MasterCraft [31]) and identified where formal methods support can
be “plugged” into the tool to make software development more ecient. How-
ever, as discussed in Section 4, there is still a lot to implement to make the tool
powerful enough to support the proposed rCOS methodology effectively, and this
is part of my current and future work. This is challenging. Yet, our discussion
shows that this is feasible. For instance:
1. With the QVT engine that is being developed at TRDDC, we can program
the expert pattern, the rule for data encapsulation and structural refinement
rules that have been proved for rCOS in [23].
2. Automatic generation of executable code is challenging, however, with the
semantics of state diagrams, sequence diagrams and textual specifications,
it is possible to generate code with control structures, method invocations,
assertions, and class invariants.
3. With human interaction, transformations for decomposing components and
composing components in the design stage can be automated.
The current version of MasterCraft does not support the design of controllers of
hardware devices and their integration with the application software components
and GUI components. However, the discussion at the end of Section 3 shows, this
is purely event-based and can be done by following the techniques of embedded
systems modelling, design and verification.
Acknowledgements. This paper is dedicated to the 70th birthdays of Pro-
fessors Dines Bjørner and Zhou Chaochen who together founded UNU-IIST in
1992. Also under the supervision of professor Zhou Chaochen, Zhiming Liu did
his master study and Xiaoshan Li his PhD degree. The work of Dines on domain
engineering and the work of Zhou on logics and calculi have great influence on
the research presented in this paper. We also thank our colleagues who have
made contributions in the development of rCOS and CoCoME, He Jifeng, Chen
Xin, Zhao Liang, Liu Xiaojian, Vladimir Mencl, Zhan Naijun, Anders Ravn and
Joseph Okika.
References
1. Apache tuscany project, http://incubator.apache.org/tuscany/
2. The concurrency workbench, http://homepages.inf.ed.ac.uk/perdita/cwb/
3. Service component architecture, http://www.osoa.org/display/Main/Home
4. Back, R.J.R., von Eright, J.: Refinement Calculus: A Systematic Introduction. In:
Graduate Texts in Computer Science, Springer, Heidelberg (1998)
5. Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley,
Reading (1988)
6. Chen, X., He, J., Liu, Z., Zhan, N.: A model of component-based programing. In:
Biryukov, A. (ed.) FSE 2007. LNCS, vol. 4593, Springer, Heidelberg (2007)