By the same authors

From the same journal

A Rigorous Method for Inspection of Model-Based Formal Specifications

Research output: Contribution to journalArticlepeer-review



Publication details

JournalIEEE Transactions on Reliability
DateE-pub ahead of print - 9 Nov 2010
DatePublished (current) - Dec 2010
Issue number4
Number of pages18
Pages (from-to)667-684
Early online date9/11/10
Original languageEnglish


Writing formal specifications can help developers understand users' requirements, and build a solid foundation for implementation. But like other activities in software development, it is error-prone, especially for large-scale systems. In practice, effective detection of specification errors still remains a challenge. In this paper, we put forward a rigorous, systematic method for the inspection of model-based formal specifications. The method makes good use of the well-defined consistency properties of a specification to provide precise rules and guidelines for inspection. The inspection process utilizes both well-defined expressions derived from the specification and human inspectors' judgments to find errors. We present a case study of the method by describing how it is applied to inspect an Automated Teller Machine (ATM) software specification to investigate the method's feasibility, and explore potential challenges in using it. We also describe a prototype software tool including its functions and distinct features to demonstrate the tool supportability of the method.

    Research areas

  • Formal analysis, formal specification, rigorous inspection, verification, SOFTWARE, REQUIREMENTS, SYSTEMS, DESIGN, SOFL, SAFETY, TOOL

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations