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.