Extending Ina Jo With Teimporal Logic

Toward the overall goal of putting formal specifications to practical use in the design of Iarge 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. Two significant contributions of a formal nature included in this paper are: (1) the definition of a unified branching temporal logic system that includes henceforth, eventually, next, and until operators and (2) a formal definition of a core of lna Jo, a specification language that has been in use since the early 1980´s. Finally, a contribution of a more practical nature is a specification of a non-trivial example--a secure communications network-- chosen to contrast assertions using temporal operators from those that use explicit time variables.