Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 8

Proceedings of the 2016 Federated Conference on Computer Science and Information Systems

ReSA Tool: Structured Requirements Specification and SAT-based Consistency-checking

, ,

DOI: http://dx.doi.org/10.15439/2016F404

Citation: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, pages 1737–1746 ()

Full text

Abstract. Most industrial embedded systems requirements are specified in unstructured natural language, hence they can sometimes be ambiguous and error-prone. Moreover, employing an early-stage model-based incremental system development using multiple levels of abstraction, for instance via architectural languages such as EAST-ADL, calls for different granularity requirements specifications described with abstraction-specific concepts that reflect the respective abstraction level effectively. In this paper, we propose a toolchain for structured requirements specification in the ReSA language, which scales to multiple EAST-ADL levels of abstraction. Furthermore, we introduce a consistency function that is seamlessly integrated into the specification toolchain, for the automatic analysis of requirements logical consistency prior to their temporal logic formalization for full formal verification. The consistency check subsumes two parts: (i) transforming ReSA requirements specification into boolean expressions, and (ii) checking the consistency of the resulting boolean expressions by solving the satisfiability of their conjunction with the Z3 SMT solver. For validation, we apply the ReSA toolchain on an industrial vehicle speed control system, namely the Adjustable Speed Limiter.

References

  1. M. Garg and R. Lai. Measuring the Constraint Complexity of Automotive Embedded Software Systems. In Data and Software Engineering (ICODSE), 2014 International Conference on, pages 1–6, Nov 2014.
  2. S. Farfeleder, T. Moser, A. Krall, T. Stlhane, H. Zojer, and C. Panis. DODT: Increasing Requirements Formalism using Domain ontologies for Improved Embedded Systems Development. In Design and Diagnostics of Electronic Circuits Systems (DDECS), 2011 IEEE 14th International Symposium on, pages 271–274, April 2011.
  3. Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, and Richard Seeber. Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, chapter RATSY – A New Requirements Analysis Tool with Synthesis, pages 425–429. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010.
  4. Constance Heitmeyer, James Kirby, Bruce Labaw, and Ramesh Bharadwaj. Computer Aided Verification: 10th International Conference, CAV’98 Vancouver, BC, Canada, June 28 – July 2, 1998 Proceedings, chapter SCR: A Toolset for Specifying and Analyzing Software Requirements, pages 526–531. Springer Berlin Heidelberg, Berlin, Heidelberg, 1998.
  5. Philippe Cuenot, Patrick Frey, Rolf Johansson, Henrik Lönn, Yiannis Papadopoulos, Mark-Oliver Reiser, Anders Sandberg, David Servat, Ramin Tavakoli Kolagari, Martin Törngren, et al. The EAST-ADL Architecture Description Language for Automotive Embedded Software. In Model-Based Engineering of Embedded Real-Time Systems, pages 297–307. Springer, 2010.
  6. Nesredin Mahmud, Cristina Seceleanu, and Oscar Ljungkrantz. ReSA: An Ontology-based Requirement Specification Language Tailored to Automotive Systems. In 10th IEEE International Symposium on Industrial Embedded Systems (SIES), pages 1–10. IEEE, jun 2015.
  7. Leonardo De Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008.
  8. Didar Zowghi and Vincenzo Gervasi. The Three Cs of Requirements: Consistency, Completeness, and Correctness. In International Workshop on Requirements Engineering: Foundations for Software Quality, Essen, Germany: Essener Informatik Beitiage, pages 155–164, 2002.
  9. M.P.E. Heimdahl and N.G. Leveson. Completeness and Consistency in Hierarchical State-based Requirements. Software Engineering, IEEE Transactions on, 22(6):363–377, Jun 1996.
  10. Constance L. Heitmeyer, Ralph D. Jeffords, and Bruce G. Labaw. Automated Consistency Checking of Requirements Specifications. ACM Trans. Softw. Eng. Methodol., 5(3):231–261, July 1996.
  11. No Silver Bullet. Essence and Accidents of Software Engineering, FP Brooks. IEEE Computer, 20(4):10–19, 1987.
  12. Elizabeth Hull, Ken Jackson, and Jeremy Dick. Requirements Engineering. Springer Science & Business Media, 2010.
  13. Andrew Radford. Minimalist Syntax: Exploring the Structure of English. Cambridge University Press, 2004.
  14. Vincent Debruyne, Françoise Simonot-Lion, and Yvon Trinquet. EAST-ADL-An Architecture Description Language. In Architecture Description Languages, pages 181–195. Springer, 2005.
  15. ATESST2 Consortium et al. EAST-ADL Domain Model Specification. ATESST2, Deliverable D, 4, 2010.
  16. TypeFox items. XText 2.5 Documentation, 2013.
  17. Lars Marius Garshol. BNF and EBNF: What are They and How Do They Work?, 2008.
  18. Jianan Yue. Transition from EBNF to Xtext. Alternation, 1:1, 2014.
  19. Devlin David and Barry OSullivan. Satisfiability as a Classification Problem. In Proc. of the 19th Irish Conf. on Artificial Intelligence and Cognitive Science. 2008.
  20. Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB Standard Version 2.0. 2010.
  21. Constance Heitmeyer, James Kirby, Bruce Labaw, and Ramesh Bharadwaj. SCR: A Toolset for Specifying and Analyzing Software Require- ments. In Computer Aided Verification, pages 526–531. Springer, 1998.
  22. Axel van Lamsweerde. Formal Specification: a Roadmap. In Proceedings of the Conference on the Future of Software Engineering, pages 147–159. ACM, 2000.
  23. Vegard Johannessen. CESAR-text vs. Boilerplates: What is More Effcient-requirements? Written as Free Text or Using Boilerplates (templates)? 2012.
  24. Alistair Mavin and Philip Wilkinson. Big Ears (The Return of “Easy Approach to Requirements Engineering”). In 2010 18th IEEE International Requirements Engineering Conference, pages 277–282. IEEE, sep 2010.
  25. Alistair Mavin, Philip Wilkinson, Adrian Harwood, and Mark Novak. Easy Approach to Requirements Syntax (EARS). In 2009 17th IEEE International Requirements Engineering Conference, pages 317–322. IEEE, aug 2009.
  26. Sascha Konrad and Betty HC Cheng. Real-time Specification Patterns. In Proceedings of the 27th international conference on Software engineering, pages 372–381. ACM, 2005.
  27. Matthew B Dwyer, George S Avrunin, and James C Corbett. Patterns in Property Specifications for Finite-state Verification. In Software Engineering, 1999. Proceedings of the 1999 International Conference on, pages 411–420. IEEE, 1999.
  28. Amalinda Post, Igor Menzel, and Andreas Podelski. Applying Restricted English Grammar on Automotive RequirementsDoes It Work? A Case Study. In Requirements Engineering: Foundation for Software Quality, pages 166–180. Springer, 2011.
  29. Andreas Mitschke. EAST-ADL Domain Model SpecificationVersion. EAST-ADL Association, 02 2012. Version 2.0.
  30. The REUSE Company. Requirements Authoring Tool, 2016.
  31. Zhou Chaochen, Charles Anthony Richard Hoare, and Anders P Ravn. A Calculus of Durations. Information processing letters, 40(5):269–276, 1991.
  32. Christian Ellen, Sven Sieverding, and Hardi Hungar. Detecting Consistencies and Inconsistencies of Pattern-based Functional Requirements. In Formal Methods for Industrial Critical Systems, pages 155–169. Springer, 2014.
  33. BTC Embedded Systems. Attempto tools, 2016.
  34. Norbert E. Fuchs and Rolf Schwitter. Attempto Controlled Natural Language for Requirements Specifications. In Proc. Seventh Intl. Logic Programming Symp. Workshop Logic Programming Environments, pages 25–32, 1995.
  35. Attempto Project. Attempto Tools, 2013.
  36. Rolf Schwitter. English as a Formal Specification Language. In Database and Expert Systems Applications, 2002. Proceedings. 13th International Workshop on, pages 228–232. IEEE, 2002.
  37. Rongjie Yan, Chih-Hong Cheng, and Yesheng Chai. Formal Consistency Checking over Specifications in Natural Languages. In Design, Automation & Test in Europe Conference & Exhibition (DATE), 2015, pages 1677–1682. IEEE, 2015.