Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Validation of formal specifications through transformation and animation
Mashkoor A., Jacquot J. Requirements Engineering22 (4):433-451,2017.Type:Article
Date Reviewed: Jan 18 2018

A validation check between a design and its implementation is usually done in order to validate the correctness of the requirements for any system. It is crucial to check that the requirements are correct when the system is developed. Formal techniques are usually used for checking the correctness of the system’s requirements.

Mashkoor and Jacquot present an approach to check the correctness of a system’s requirements using formal specifications through transformation and animation. They propose a framework, called verify-transform-animate (VTA), for their approach.

The authors’ approach starts by formalizing the specification requirements of any system by grouping them into observation levels. Then, the formal specification is verified through model checking. Finally, once the formal specification is verified, the specification is transformed into a model using animation. Animation is used to demonstrate the behavior of the specification to stakeholders after its correctness is verified.

The authors demonstrate the proposed approach using case studies and successfully proving the case studies in terms of the validation of formal requirements specifications. The evaluation shows the correctness of the animated specifications. The VTA framework can be used by readers to transform the requirements of any system into animated specifications, for easy demonstrations for stakeholders.

Reviewer:  Rosziati Ibrahim Review #: CR145785 (1803-0147)
Bookmark and Share
 
Formal Methods (D.2.4 ... )
 
 
Validation (D.2.4 ... )
 
 
Requirements/ Specifications (D.2.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
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