Miro Research Description.

摘要

The heart of the proposed research lies in the formal specification of complex software systems. We are interested in specifying not just the functional correctness of a system, but also its behavior imposed by concurrency, fault-tolerance, security, and real-time constraints. Current specification techniques are inadequate for describing such behavior for realistic, large-scaled systems. We need to combine isolated research results from the areas of formal specifications and formal models of concurrency, and more significantly, to extend them in order to specify properties that are as critical as functional correctness. The novel aspect of this research is to exploit the benefits of visual languages to specify system behavior. We intend to design a visual specification language; to give a formal semantics to the language; to build a rich set of tools for presenting and manipulating visual specifications; and to demonstrate the suitability of the language to the specification of a wide class of system properties.