In: Proc. Int. Symp. on Software Engineering for Parallel and Distributed Systems, 17-18 May 1999, Los Angeles, CA, pages 38-51. 1999.
Abstract: The ability to check whether the modeled system satisfies certain properties is a very important aspect in the software development process. Many object-oriented methods do not pay enough attention to the behavioral descriptions. Indeed, they mostly do not provide formally founded descriptions that can be checked automatically. This paper presents an integrated approach, consisting of formally founded description techniques, an expressive temporal logic for specifying properties, and a model checking mechanisms for automatically checking whether some executions of the specified system satisfy the required properties.
Keywords: Petri nets, distributed systems, model checking, object-oriented systems, system specification, temporal logic.