|
Formal Methods for Systems and Software Specifications
|
|
Point of Contact
|
Caroline Wang
Caroline.K.Wang@nasa.gov
|
|
Dates
|
January 2009 - December 2011
|
|
Problem
|
Research shows that organizations spend 33% to 50% of their total cost of developing and maintaining a system by preparing for or recovering from failures. This figure is higher for "High Consequence" or "High Critical" systems such as NASA's manned space flight and high dollar unmanned space programs. Furthermore, failures during test as a result of an improperly specified user need or system requirement not only increases cost due to rework and retest but results in a less than optimal design which increase maintenance costs in the future. It is a common known fact that improperly specified requirements will yield a system that does not meet the customer needs and could in fact contain latent defects or design flaws which could have Catastrophic results. Therefore, ensuring software requirements are complete, accurate, correct, and consistent is beneficial for reducing overall program cost and risk and safety risk. Formal methods provide a framework for specifying requirements in mathematical notation which can then be modeled and proven as complete, accurate, correct, and consistent.
Formal methods are mathematically based techniques for specification, development and verification of systems, both hardware and software. The specifications used in formal methods are well-formed statements expressed in a mathematical logic. The use of formal methods approaches can help to eliminate errors early in the design process. Practitioners have also recognized that they can make searching for reusable components more effective by having formal specifications of components.
The mathematics of formal methods is based on notations and concepts from basic set theory and propositional and predicate logics. These are basic mathematics requirements for undergraduate study in engineering and science and therefore well-know to practicing engineers and scientists.
There are significant returns from applying formal methods. They have potential use in clarifying test criteria, identifying potential bottlenecks and ensuring good test coverage and even automating testing. Software that was developed using formal methods has been demonstrated to be more reliable and more suitable for reuse. A requirement specification written in a "Formal Language" instead of a "Natural Language" is more accurate and unambiguous which results in a more reliable system which in turn can be validated much more efficient and effectively.
|
|
Objective
|
The goals of this research are to:
- investigate various formal methods techniques for practical usefulness and applicability to critical NASA software development activities; and
- develop techniques, processes, and training material which can be used by software engineers' (both developers and V&V) for applying formal methods on a development program.
This research supports NASA?s Software Initiative strategies on improving safety, reliability, and quality of software.
The objectives for this research are:
Define Case Studies for multiple projects (Using current NASA, DoD projects).
Identify specific capabilities within project that will be modeled.
Refreshing knowledge of Formal Methods, ?B? language, and learning additional Formal Notation languages, and tools.
Translate the software requirements for the selected capabilities from natural language to Formal Methods language.
Evaluate various formal methods tools, document pros and cons for various tools, and select the most appropriate tool for this project.
Model the selected capability requirements in the selected tool, develop obligation proofs, and test the case studies.
Generate reports, and develop guide book.
Develop Training program to educate NASA Scientists and Engineers in developing requirements by using Formal Methods.
Execute the training program.
|
|
Results
|
No results are available at this time. Please check back again.
|
|
Keywords
|
Formal Methods, Software Specification, Guidebook
|
|
Categories
|
Formal Methods
Requirements Analysis
|
|
