Automated formal methods for reliable software components

在我的研究计划中，我从事软件验证，这是一种将程序作为输入并就程序中可能存在的错误向用户提供反馈的方法。我们今天已经在我们的编译器中使用了这样的技术：它们分别根据变量和函数的类型和签名检查我们是否正确地使用了它们。作为迈向无错误程序的最终目标的下一步，我们开发了检查语义属性所需的技术，例如，堆上的数据结构是否一致，或者在程序执行期间是否可能有一些被禁止的变量值。理论上，这些检查是无法决定的，但在实践中，由于最近程序验证方面的几项突破，我们有很大希望实际上可以验证许多有趣的性质。这个问题被认为是计算机科学中的一个巨大挑战，只有许多研究小组共同做出巨大努力，才能开发出最终可能实现软件工程理想的所有技术：经过验证的软件。然而，并不总是能够获得我们系统所有组件的源代码。如果我们构建基于Web服务的信息系统，这种现象自然会发生。由不同开发团队开发的不同组件在不同的位置和不同的计算机平台上运行。对于某些组件的检查或内部测试，无法获得源代码或可执行程序。在提出的研究中，我们致力于一种新的形式化方法，称为Web服务接口，以简洁的方式制定Web服务的规范，并开发一个支持基于我们的语言的Web服务建模和分析的工具平台。然后，Web服务的提供者可以向客户端提供其服务的正式接口。提供者可以使用该接口来检查实际实现是否实现了该接口所做的所有承诺。Web服务的客户端可以使用所提供的接口来检查客户端组件是否与该接口兼容。如果两者都给出，那么总体构图肯定会起作用。我们将为这两项任务提供自动程序。

In my research program I work on software verification, which is a method that takes as input a program and gives the user feedback about possible bugs in the program. We already use such techniques today, in our compilers: they check if we use all variables and functions properly, according to their types and signatures, respectively. As a next step towards the ultimate goal of error-free programs, we develop the technology needed for checking semantical properties, e.g., if data structures on the heap are consistent, or if some forbidden variable value is possible during program execution. Theoretically, these checks are undecidable, but in practice, due to several recent breakthroughs in program verification, there is a strong hope that we can actually verify many interesting properties. The problem is identified and widely acknowledged as a grand challenge in computer science, and only an enormous effort of many research groups together can develop all the techniques that at the end make it possible to achieve the ideal of software engineering: verified software.     However, it is not always possible to obtain the source code for all components of our system. This phenomenon naturally occurs if we build information systems based on web services. Different components, developed by different development teams, are running at different locations and on different computer platforms. Neither the source code nor the executable program is obtainable for inspection or in-house testing of certain components. In the proposed research, we are working on a new formalism, called web service interfaces, to formulate specifications of web services in a concise way, and develop a tool platform that supports modeling and analysis of web services based on our language. A provider of a web service can then offer to the clients a formal interface of its service. The provider can use the interface to check if the actual implementation fulfills all promises made by the interface. The client of the web service can use the provided interface to check if the client component is compatible with the interface. If both is given, then the overall composition is guaranteed to work. We will provide automatic procedures for both tasks.