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.