Introduction - lgwagner/SpeAR GitHub Wiki
This is a User Guide for SpeAR (Specification and Analysis of Requirements) v2.0 [1], an open-source tool for capturing and analyzing requirements stated in a language that is formal, yet designed to read like natural language.
Requirements capture and analysis is a challenging problem for complex systems and yet is fundamental to ensuring development success. Traditionally, requirements suffer from unavoidable ambiguity that arises from reliance on natural language. Formal methods mitigates this ambiguity through mathematical representation of desired behaviors and enables analysis and proofs of properties.
SpeAR allows systems engineers to capture requirements in a language with the formal semantics of Past Linear Temporal Logic (Past LTL) [2] and supports proofs of critical properties about requirements using model checking [3]. Moreover, the SpeAR user interface performs validations, including type-checking, that provide systems engineers with real-time feedback on the well-formedness of requirements. Initial feedback from systems engineers has been positive, emphasizing the readability of the language. Additionally, our use of SpeAR on early case studies has identified errors and omissions in captured requirements.
This User Guide Wiki contains several sections. The Installation Instructions Section provides installation instructions for SpeAR and the supporting tools. Overview of SpeAR provides a description of the important elements in a SpeAR specification. The Using SpeAR Section shows the user how to create and import projects, develop a new specification using the SpeAR File Wizard, and run analysis. Complex Example presents a more complex example with a hierarchical specifications. Software Engineering Process Inclusion describes SpeAR features that support SpeAR’s inclusion in the software engineering process. These features include capturing requirement attribute information, exporting an Excel spreadsheet of the requirements, and performing traceability analysis on the requirements set. Language Description provides a complete grammar description. Analyses explains how each kind of SpeAR analysis works. Finally, Configuration of SpeAR Preferences explains the configuration options available to the user.
- ^ https://github.com/lgwagner/SpeAR
- ^ Cimatti, A., Roveri, M., Sheridan, D.: Bounded Verification of Past LTL, pp. 245-259. Springer Berlin Heidelberg (2004)
- ^ Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT press (2008)