The increased reliance on software in critical applications suggests a greater need for formal methods to be used in the development of such software. A number of formal languages and toolsets exist for developing formally specified and verified software; however experience tells us that the development of formally verified software, even with the current tool support, is an expensive process.By adopting a component-based development methodology, whereby software is developed from reusable components, significant savings can be made. In particular the amount of proof --- arguably the most expensive and difficult part of formal development --- can be greatly reduced by proving the correctness of reusable components once, off-line, prior to their use.Tools are required which support the user in adapting and retrieving components from libraries of formally specified components. This paper describes extensions to the CARE toolset that support adaptation and retrieval of reusable components.
展开▼
机译：在关键应用程序中对软件的依赖性越来越高，这表明在开发此类软件时更需要使用正式方法。存在许多用于开发正式指定和验证的软件的形式语言和工具集;但是，经验告诉我们，即使使用当前的工具支持，正式验证软件的开发也是一项昂贵的过程。通过采用基于组件的开发方法，即从可重复使用的组件开发软件，可以节省大量资金。尤其是可以通过在使用前离线验证可重复使用组件的正确性来大大减少证明的数量-可以说是正式开发中最昂贵和最困难的部分-所需的工具需要支持用户从正式指定的组件库中改编和检索组件。本文介绍了C ARE 工具集的扩展，这些工具集支持对可重用组件的适应和检索。
展开▼
