9804091 This project focuses on the development of effective specification formalisms for component-oriented, or open, concurrent systems. The specific topics addressed include: the investigation of implicit specifications for open systems; and the development of efficient yet generic model-checking techniques for temporal logics, including those for open systems. Implicit specifications take form of contexts, or system descriptions with "holes," into which the component being developed is to be inserted. The motivation for such specifications is practical: they may be written using the same notation in which the system description is given and do not require users to learn additional logical notations. This project investigates the expressiveness of, and case studies involving, such specifications. Model checkers permit the automatic determination of when systems enjoy properties in temporal logics. The results of this part of the project will show how generic yet efficient model-checking procedures that work for all temporal logics may be given; this will improve on the existing state of the art, which requires new procedures for each new logic. The project as a whole will yield results leading to improved automated methodologies, and hence better analysis tools, for specifying and reasoning about component- oriented concurrent software.***
