Featured Topic Issue — Best Papers from SEKE 2016; Guest Editor: Jerry GaoNo Access

An Algorithm for Forward Reduction in Sequence-Based Software Specification

Lan Lin

Department of Computer Science, Ball State University, Muncie, IN 47306, USA

E-mail Address: llin4@bsu.edu

Search for more papers by this author

Yufeng Xue

Department of Computer Science, Ball State University, Muncie, IN 47306, USA

E-mail Address: yxue2@bsu.edu

Search for more papers by this author

, and

Fengguang Song

Department of Computer and Information Science, Indiana University–Purdue University Indianapolis, Indianapolis, IN 46202, USA

E-mail Address: fgsong@cs.iupui.edu

Search for more papers by this author

https://doi.org/10.1142/S0218194016400118Cited by:0 (Source: Crossref)

Abstract

Sequence-based software specification is a rigorous method for deriving a formal system model based on informal requirements, through a systematic process called sequence enumeration. Under this process, stimulus (input) sequences are considered in a breadth-first manner, with the expected system response to each sequence given. Not every sequence needs to be further extended by the enumeration rules. The completed specification encodes a Mealy machine and forms a basis for other activities including code development and testing. This paper presents a forward reduction algorithm for sequence-based specification. The need for such an algorithm has been identified by field applications. We used the state machine as an intermediate tool to comprehend and analyze all change impacts resulted from a forward reduction, and used an axiom system for its development. We present the algorithm both mathematically in functional form and procedurally in pseudocode, illustrate it with a symbolic example, and report a larger case study from the published literature in which the algorithm is applied. The algorithm will prove useful and effective in deriving a system-level specification as well as in merging and combining partial work products towards a formal system model in field applications.

Keywords:

References

1. J. H. Poore, private communication, 2010. Google Scholar
2. UTK-SQRL, Prototype Sequence Enumeration (Proto_Seq) (2016), Software Quality Research Laboratory, The University of Tennessee, https://sourceforge.net/projects/protoseq/. Google Scholar
3. UTK-SQRL, Requirements Elicitation and Analysis with Sequence-Based Specification (REALSBS) (2016), Software Quality Research Laboratory, The University of Tennessee, http://realsbs.sourceforge.net. Google Scholar
4. W. Bartussek and D. L. Parnas, Using assertions about traces to write abstract specifications for software modules, in Proc. 2nd Conf. European Cooperation on Informatics, 1978, pp. 211–236. Google Scholar
5. T. Bauer, T. Beletski, F. Boehr, R. Eschbach, D. Landmann and J. Poore, From requirements to statistical testing of embedded systems, in Proc. 4th Int. Workshop on Software Engineering for Automotive Systems, 2007, pp. 3–9. Google Scholar
6. S. Ben-David, M. Chechik and S. Uchitel, Merging partial behaviour models with different vocabularies, in Proc. 24th Int. Conf. Concurrency Theory, 2013, pp. 91–105. Google Scholar
7. L. Bouwmeester, G. H. Broadfoot and P. J. Hopcroft, Compliance test framework, in Proc. 2nd Workshop on Model-Based Testing in Practice, 2009, pp. 97–106. Google Scholar
8. G. H. Broadfoot and P. J. Broadfoot, Academia and industry meet: Some experiences of formal methods in practice, in Proc. 10th Asia-Pacific Software Engineering Conf., 2003, pp. 49–59. Google Scholar
9. J. Brzozowski, Derivatives of regular expressions, J. ACM 11 (4) (1964) 481–494. Crossref, Web of Science, Google Scholar
10. J. Brzozowski, Representation of a class of nondeterministic semiautomata by canonical words, Theor. Comput. Sci. 356 (2006) 46–57. Crossref, Web of Science, Google Scholar
11. J. Brzozowski and H. Jürgensen, Representation of semiautomata by canonical words and equivalences, Int. J. Found. Comput. Sci. 16 (5) (2005) 831–850. Link, Web of Science, Google Scholar
12. J. Brzozowski and H. Jürgensen, Representation of semiautomata by canonical words and equivalences, part II: Specification of software modules, Int. J. Found. Comput. Sci. 18 (5) (2007) 1065–1087. Link, Web of Science, Google Scholar
13. D. Fischbein, N. D’ippolito, G. Brunet, M. Chechik and S. Uchitel, Weak alphabet merging of partial behavior models, ACM Trans. Softw. Eng. Methodol. 21 (2) (2012) 9:1–9:47. Crossref, Web of Science, Google Scholar
14. C. L. Heitmeyer, Software cost reduction, in Encyclopedia of Software Engineering, ed. J. J. Marciniak (John Wiley and Sons, 2002), pp. 1374–1380. Crossref, Google Scholar
15. P. J. Hopcroft and G. H. Broadfoot, Combining the box structure development method and CSP for software development, Electron. Notes Theor. Comput. Sci. 128 (6) (2005) 127–144. Crossref, Google Scholar
16. D. Jackson, M. Thomas and L. I. Millett (eds.), Software for Dependable Systems: Sufficient Evidence? (National Academies Press, 2007). Google Scholar
17. R. Janicki and E. Sekerinski, Foundations of the trace assertion method of module interface specification, IEEE Trans. Softw. Eng. 27 (7) (2001) 577–598. Crossref, Web of Science, Google Scholar
18. M. Joseph, (ed.), Real-Time Systems: Specification, Verification and Analysis (Prentice-Hall International, London, 1996). Google Scholar
19. F. Khendek and G. V. Bochmann, Merging behavior specifications, Form. Methods Syst. Des. 6 (3) (1995) 259–293. Crossref, Web of Science, Google Scholar
20. L. Lin, S. J. Prowell and J. H. Poore, The impact of requirements changes on specifications and state machines, Softw., Pract. Exp. 39 (6) (2009) 573–610. Crossref, Web of Science, Google Scholar
21. L. Lin, S. J. Prowell and J. H. Poore, An axiom system for sequence-based specification, Theor. Comput. Sci. 411 (2) (2010) 360–376. Crossref, Web of Science, Google Scholar
22. R. C. Linger, H. D. Mills and B. I. Witt, Structured Programming: Theory and Practice (Addison-Wesley, 1979). Google Scholar
23. H. D. Mills, The new math of computer programming, Commun. ACM 18 (1) (1975) 43–48. Crossref, Web of Science, Google Scholar
24. H. D. Mills, Stepwise refinement and verification in box-structured systems, Computer 21 (6) (1988) 23–36. Crossref, Web of Science, Google Scholar
25. S. Nejati, M. Sabetzadeh, M. Chechik, S. Easterbrook and P. Zave, Matching and merging of variant feature specifications, IEEE Trans. Softw. Eng. 38 (6) (2012) 1355–1375. Crossref, Web of Science, Google Scholar
26. D. L. Parnas and Y. Wang, The trace assertion method of module interface specification, Technical Report No. 89-261, Queens University (1989). Google Scholar
27. S. J. Prowell and J. H. Poore, Sequence-based software specification of deterministic systems, Softw., Pract. Exp. 28 (3) (1998) 329–344. Crossref, Web of Science, Google Scholar
28. S. J. Prowell and J. H. Poore, Foundations of sequence-based software specification, IEEE Trans. Softw. Eng. 29 (5) (2003) 417–429. Crossref, Web of Science, Google Scholar
29. S. J. Prowell and W. T. Swain, Sequence-based specification of critical software systems, in Proc. 4th American Nuclear Society Int. Topical Meeting on Nuclear Plant Instrumentation, Controls and Human-Machine Interface Technology, 2004. Google Scholar
30. S. J. Prowell, C. J. Trammell, R. C. Linger and J. H. Poore, Cleanroom Software Engineering: Technology and Process (Addison-Wesley, Reading, 1999). Google Scholar
31. S. Uchitel and M. Chechik, Merging partial behavioral models, in Proc. 12th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, 2004, pp. 43–52. Google Scholar