SpeAR: Specification and Analysis of Requirements

Abstract

Traditional safety-critical software development methods focus on the sequential activities of specification, design, implementation, and verification. The inherent weakness in this approach is that any specification or design errors found in verification require rework through all steps of the process. This is compounded by the growing complexity of software, often resulting in substantial software development overruns in safety-critical applications. In this paper we introduce a formalized requirements development framework named Specification and Analysis of Requirements (SpeAR) that is designed to help users develop more precise specifications which are formally constructed and enable analysis early in system development. SpeAR provides a set of commonly used patterns as a front-end for behavioral specification and a suite of analyses on the back-end to ensure the resulting specification is logically consistent. This paper will discuss the features of SpeAR and briefly discuss one industrial effort in which it was used to specify and analyze requirements.

1 Butler, R. W. “Langley Formal Methods” NASA Langley Research Center, Virginia, 24 January 2008. [http://shemesh.larc.nasa.gov/fm/index.html. Accessed 5/28/13]
2 Butler, R. W. “What is Formal Methods?” NASA Langley Research Center, Virginia, 6 August 2001. [http://shemesh.larc.nasa.gov/fm/index.html. Accessed 5/28/13]
3 Butler, R. W. “Why is Formal Methods Necessary?” NASA Langley Research Center, Virginia, 6 May 2004. [http://shemesh.larc.nasa.gov/fm/fm-why-new.html. Accessed 5/28/13]
4 Alavi, H., Avrunin, G., Corbett, J., Dillon, L., Dwyer, M., Pasareanu, C., “Spec Patterns,” SAnToS Laboratory at Kansas State University. [http://patterns.projects.cis.ksu.edu/. Accessed 5/30/13]
5 Dwyer, Matthew, George Avrunin, and James Corbett. "Patterns in Property Specifications for Finite-State Verification." Proceedings of the 21st International Conference on Software Engineering. (1999)
6 Axe, David. "Pentagon: Trillion-Dollar Jet on the Brink of Budgetary Disaster." Wired. 03 Mar 2012. Web. 16 Oct 2013. <http://www.wired.com/dangerroom/2012/03/f35-budget-disaster/>.
7 Bloem, Roderick, Roberto Cavada, Ingo Pill, Marco Roveri, and Andrei Tchaltsev. "RAT: a tool for the formal analysis of requirements." Proceedings of the 19th International Conference on Computer Aided Verification. (2007): 263-267.

Presenter Bio

Lucas Wagner is a Senior Systems Engineer with Rockwell Collins’ Advanced Technology Center. His principal area of expertise is applying formal analysis techniques, particularly model checking, to industrial problems. His background includes developing methods and tools to integrate formal methods into industrial development processes and design of realtime embedded systems for safety-critical applications.

Most recently, he has led an effort sponsored by AFRL to transition formal methods into the entire development process, from specification to system integration and verification. On this effort he led the development of SpeAR, a requirements formalization and analysis framework.