Graphical Tools for Development of Concurrent Systems

计算机科学的最大挑战之一是为实际应用开发正确的程序。最关键的实际应用程序通常涉及并行处理、并发和实时。这些特征降低了当前软件工程技术的有效性，并强调了对更正式方法的需求。图形区间逻辑源于S4.3模式逻辑，与软件工程师绘制的时序图非常相似，因此非常直观和易于使用。以图形方式表示的并发系统规范可以解析为内部模式表示，并提交给定理证明者，以提供对程序或系统设计的预期属性的严格确认。这个项目将开发一个图形区间逻辑的实验实现及其相关的规范数据库、解析器和定理证明器，并将研究该逻辑在Ada程序验证和测试中的应用。这些工具将与工业伙伴协商设计，并将由他们评估在实际应用中的使用情况。

One of the great challenges of computer science is the development of correct programs for real applications. The most critical real applications often involve parallel processing, concurrency, and real time. These characteristics render current techniques of software engineering less effective and emphasize the need for more formal methods. Graphical Interval Logic derived from S4.3 modal logic, closely resembles the timing diagrams drawn by software engineers and, thus, is highly intuitive and easy to use. Specifications expressed graphically for concurrent systems can be parsed into an internal modal representation and submitted to a theorem prover to provide rigorous confirmation of the intended properties of a program or system design. This project will develop an experimental implementation of Graphical Interval Logic with its associated specification database, parser, and theorem prover, and will investigate the application of the logic to the verification and testing of Ada programs. The tools will be designed in consultation with industrial partners and will be evaluated by them for use in real applications.