Model programs are high-level behavioral specifications used for software testing and design analysis. Composition of model programs is a versatile technique that, at one end of the spectrum, enables one to build up larger models from smaller ones, and at the other end of the spectrum allows one to restrict larger models to specific scenarios. In this paper we provide a formal foundation for composition of model programs and investigate its use in various situations that arise in model program analysis.

PDF file

In  The Journal of Logic and Algebraic Programming

Publisher  Elsevier
Copyright © 2007 Elsevier B.V. All rights reserved.

Details