Abstract
We propose a collaboration project to integrate the research effort and results obtained at UNU-IIST on formal techniques in component and object systems with research at TRDDC in modelling and development of tools that support object-oriented and component-based design. The main theme is an integration of verification techniques with engineering methods of modelling and design, and an integration of verification tools and transformation tools. This will result in a method in which a correct program can be developed through transformations that are either proven to be correct or by showing that the transformed model can be proven correct by a verification tool.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Mastercraft. Tata Consultancy Services, http://www.tata-mastercraft.com
Aichernig, B.K., He, J., Liu, Z., Reed, M.: Theories and techniques of program modelling, design and verification. In: IFIP Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE) (2005)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns, Elements of Reusable Object-Oriented Software. Addlison Wesley, London (1994)
He, J.: Link simulation with refinement. In: Proc. of The 25th anniversary of CSP (2004)
He, J., Li, X., Liu, Z.: Component-based software engineering – the need to link methods and their theories. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 72–97. Springer, Heidelberg (2005)
Hoare, A.C.R., Misra, J.: Verified software: Theories, tools and experiments. In: The Grand Challenge Paper at the IFIP Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Zurich (October 10-13, 2005), http://vstte.ethz.ch/
Hoare, C.A.R.: The verifying compiler: A grand challenge for computer research. Journal of the ACM 50(1), 63–69 (2003)
Joseph, M.: Formal techniques in large scale software engineering. In: Keynote at IFIP Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Zurich (October 10-13, 2005), http://vstte.ethz.ch/
Kruchten, P.: The Rational Unified Process – An Introduction, 2nd edn. Addison-Wesly, London, UK (2000)
Larman, C.: Applying UML and Patterns. Prentice-Hall, Englewood Cliffs (2001)
Li, X., Liu, Z., He, J., Long, Q.: Generating prototypes from a UML model of requirements. In: International Conference on Distributed Computing and Internet Technology(ICDIT2004), Bhubaneswar, India. LNCS, Springer, Heidelberg (2004)
Liu, Z., He, J., Li, X.: Contract-oriented development of component systems. In: Proceedings of IFIP WCC-TCS2004, Toulouse, France, pp. 349–366. Kluwer Academic Publishers, Boston (2004)
Liu, Z., He, J., Li, X.: rCOS: A refinement calculus for object systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 183–221. Springer, Heidelberg (2005)
Liu, Z., He, J., Li, X., Chen, Y.: A relational model for object-oriented requirement analysis in UML. In: Proc. of International Conference on Formal Engineering Methods, Singapore, November 2003. LNCS, Springer, Heidelberg (2003)
Liu, Z., Ravn, A.P., Li, X.: Unifying proof methodologies of Duration Calculus and Linear Temporal Logic. Formal Aspects of Computing 16(2) (2004)
Long, Q., Liu, Z., He, J., Li, X.: Consistent code generation from uml models. In: Australia Conference on Software Engineering (ASWEC), IEEE Computer Scienty Press, Los Alamitos (2005)
Long, Q., Qiu, Z., Liu, Z., Shao, L., He, J.: POST: A case study for an incremental development in rCOS. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 485–500. Springer, Heidelberg (2005)
Mellor, S.J., Valcer, M.J.: Executable UML: a foundation for model-driven architecture. Addison-Wesley, Reading (2002)
OMG. The Unified Modeling Language (UML) Specification - Version 1.4, Joint submission to the Object Management Group (OMG) (September 2001) http://www.omg.org/technology/uml/index.htm
Pnueli, A.: Looking ahead. In: Workshop on The Verification Grand Challenge 2005 SRI International, Menlo Park, CA(February 21–23)
Rushby, J.: Integrating verification components. In: Keynote at IFIP Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Zurich, (October 10-13, 2005), http://vstte.ethz.ch/
Shrotri, U., Bhaduri, P., Venkatesh, R.: Model checking visual specification of requirements. In: International Conference on Software Engineering and Formal Methods (SEFM 2003), Australia, 3003., pp. 202–209. IEEE Computer Society Press, Los Alamitos
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Liu, Z., Venkatesh, R. (2008). Methods and Tools for Formal Software Engineering. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)