Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Modelling timed reactive systems from natural-language requirements
Carvalho G., Cavalcanti A., Sampaio A. Formal Aspects of Computing28 (5):725-765,2016.Type:Article
Date Reviewed: Mar 7 2017

Automated verification of software systems is an important area of current research in both academia and industry. Such methods have the potential to considerably reduce the cost of verification. Such techniques, however, depend on having a formal representation of the system specification, which can be used as a “golden model” or “oracle” from which tests can be generated. Given such a formal representation, a plethora of methods and techniques developed over the last few decades provide a high degree of automation in the verification process. However, formal specifications of systems are the exception rather than the rule in current engineering practice. This limits the applicability of the vast amount of research in formal methods for verification of real-life systems.

This paper addresses this particular gap of constructing a formal representation from an informal specification. The paper limits the scope of the problem to specifications of reactive systems; this is an important class of systems for which the benefits of automated and formal verification has been demonstrated in practice. They also take advantage of the formal nature of specification documents. Such documents use particular idioms and phrases to reduce the contextual ambiguity inherent in natural language sentences to propose a controlled natural language grammar that can be used for specification documents.

The process of constructing a formal model involves first using case grammar theory to parse a sentence into its components (agents, conditions, values, and so on). Each sentence is parsed into a requirement frame. The authors then outline algorithms to translate them into the formalism of a dataflow reactive system (DFRS), which is expressive enough to describe state transitions and delays. Two variants of the DFRS formalism are discussed: a symbolic variant, which is useful as a target of parsing natural language specifications, and an explicit variant, which is more suitable for analysis using algorithms.

Reviewer:  Prahladavaradan Sampath Review #: CR145103 (1705-0281)
Bookmark and Share
 
Formal Models Of Communication (E.4 ... )
 
 
Systems Specification Methodology (C.0 ... )
 
 
Formal Definitions And Theory (D.3.1 )
 
 
Grammars And Other Rewriting Systems (F.4.2 )
 
 
Natural Language Processing (I.2.7 )
 
 
Requirements/ Specifications (D.2.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Models Of Communication": Date
Statistical and inductive inference by minimum message length (Information Science & Statistics)
Wallace C., Springer-Verlag New York, Inc., Secaucus, NJ, 2005.  432, Type: Book (9780387237954)
Jan 17 2006
A different approach to finding the capacity of a Gaussian vector channel
Tsybakov B. Problems of Information Transmission 42(3): 183-196, 2006. Type: Article
Oct 15 2007
Stochastic recovery problem
Darkhovsky B. Problems of Information Transmission 44(4): 303-314, 2008. Type: Article
May 21 2009
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy