Adding Temporal Logic to Ina Jo

CMU-CS-85-146

Jeannette M. Wing, Mark R. Nixon oot System Development Corporation, Santa Monica, CA.

July 1985

Toward the overall goal of putting formal specifications to practical use in the design of large systems, we explore the combination of two specification methods: using temporal logic to specify concurrency properties and using an existing specification language, Ina Jo, to specify functional behavior of nondeterministic systems. In this paper, we give both informal and formal descriptions of both current Ina Jo and Ina Jo enhanced with temporal logic. We include details of a simple example to demonstrate the use of the proof system and details of an extended example to demonstrate the expressiveness of the enhanced language. We discuss at length our language design goals, decisions, and their implications. The appendices contain complete proofs of derived rules and theorem schemata for the enhanced formal system.

55 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu