×

Applying string-rewriting to sequence-based specification. (English) Zbl 1291.68255

Summary: Sequence-based specification is a constructive method designed to convert ordinary functional requirements (that are often imprecisely and informally composed) into precise specifications. The method prompts a human requirements analyst to make the many decisions necessary to resolve the ambiguities, omissions, inconsistencies, and errors inherent in the original requirements document, and construct a complete, consistent, and traceably correct specification. We find that string-rewriting theory can be applied to make a number of these decisions automatically. In this paper we develop a method of applying string-rewriting to sequence enumeration. We give prescriptions on how prefix rewrite rules and general string rewrite rules can be declared, and used later in the process to automatically make new equivalences thereby prompting the human for fewer decisions. Based on the results we present an enhanced enumeration process, in which one develops working enumerations and working reduction systems concurrently, applying string-rewriting to deduce new reductions as needed, until a complete enumeration is obtained. We present data from four published applications that shows the feasibility and applicability of applying string-rewriting. In addition to effort reduction we have observed the benefit of eliminating rework achieved by consistent decisions, as well as an additional opportunity string-rewriting provides for validation of specification decisions to requirements.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q42 Grammars and rewriting systems
Full Text: DOI

References:

[1] Bartussek, W.; Parnas, DL, Using assertions about traces to write abstract specifications for software modules, Venice, Italy
[2] Bauer, T.; Beletski, T.; Boehr, F.; Eschbach, R.; Landmann, D.; Poore, J., From requirements to statistical testing of embedded systems, Minneapolis, MN · doi:10.1109/SEAS.2007.5
[3] Book RV, Otto F (1993) String-rewriting systems. Springer, Berlin · Zbl 0832.68061 · doi:10.1007/978-1-4613-9771-7
[4] Broadfoot, GH; Broadfoot, PJ, Academia and industry meet: some experiences of formal methods in practice, Chiang Mai, Thailand
[5] Brzozowski J (1964) Derivatives of regular expressions. J ACM 11(4):481-494 · Zbl 0225.94044 · doi:10.1145/321239.321249
[6] Brzozowski J, Jürgensen H (2004) Theory of deterministic trace-assertion specifications. Technical report CS-2004-30, University of Waterloo
[7] Brzozowski J, Jürgensen H (2005) Representation of semiautomata by canonical words and equivalences. Int J Found Comput Sci 16(5):831-850 · Zbl 1080.68050 · doi:10.1142/S0129054105003327
[8] Brzozowski J, Jürgensen H (2007) Representation of semiautomata by canonical words and equivalences, part II: specification of software modules. Int J Found Comput Sci 18(5):1065-1087 · Zbl 1202.68221 · doi:10.1142/S0129054107005133
[9] Carter JM (2009) Sequence-based specification of embedded systems, Dissertation, University of Tennessee, Knoxville
[10] Carter, JM; Lin, L.; Poore, JH, Automated functional testing of Simulink control models, Berlin, Germany
[11] Eschbach R, Lin L, Poore JH (2012) Applying string-rewriting to sequence-based specification, Technical report UT-CS-12-692, University of Tennessee, Knoxville. http://web.eecs.utk.edu/ library/TechReports/2012/ut-cs-12-692.pdf · Zbl 1291.68255
[12] Hoffman D (1985) The trace specification of communications protocols. IEEE Trans Comput C34(12):1102-1113 · Zbl 0568.68024 · doi:10.1109/TC.1985.6312209
[13] Hoffman D, Snodgrass RT (1988) Trace specifications: methodology and models. IEEE Trans Softw Eng 14(9):1243-1252 · doi:10.1109/32.6168
[14] Hopcroft PJ, Broadfoot GH (2005) Combining the box structure development method and CSP for software development. Electron Notes Theor Comput Sci 128(6):127-144 · Zbl 1272.68111 · doi:10.1016/j.entcs.2005.04.008
[15] Janicki R, Sekerinski E (2001) Foundations of the trace assertion method of module interface specification. IEEE Trans Softw Eng 27(7):577-598 · doi:10.1109/32.935852
[16] Joseph M (ed) (1996) Real-time systems: specification, verification and analysis. Prentice Hall International, London · Zbl 0909.68001
[17] Lin L, Prowell SJ, Poore JH (2009) The impact of requirements changes on specifications and state machines. Softw Pract Exp 39(6):573-610 · doi:10.1002/spe.907
[18] Lin L, Prowell SJ, Poore JH (2010) An axiom system for sequence-based specification. Theor Comput Sci 411(2):360-376 · Zbl 1187.68316 · doi:10.1016/j.tcs.2009.06.041
[19] Linger RC, Mills HD, Witt BI (1979) Structured programming: theory and practice. Addison-Wesley, Boston · Zbl 0488.68007
[20] McLean J (1984) A formal method for the abstract specification of software. J ACM 31(3):600-627 · Zbl 0628.68013 · doi:10.1145/828.829
[21] Mills HD (1975) The new math of computer programming. Commun ACM 18(1):43-48 · Zbl 0293.68013 · doi:10.1145/360569.360659
[22] Mills HD (1988) Stepwise refinement and verification in box-structured systems. IEEE Comput 21(6):23-36 · doi:10.1109/2.948
[23] MPCS (2012) Mine pump controller software enumeration. http://sqrl.eecs.utk.edu/btw/files/MPCS_sr.html. Accessed 4 January 2013 · Zbl 1272.68111
[24] Parnas DL, Wang Y (1989) The trace assertion method of module interface specification, Technical report 89-261, Queens University
[25] Proto_Seq (2012) ESP project. http://sqrl.eecs.utk.edu/esp/index.html. Accessed 4 January 2013
[26] Prowell SJ, Poore JH (1998) Sequence-based software specification of deterministic systems. Softw Pract Exp 28(3):329-344 · doi:10.1002/(SICI)1097-024X(199803)28:3<329::AID-SPE157>3.0.CO;2-H
[27] Prowell SJ, Poore JH (2003) Foundations of sequence-based software specification. IEEE Trans Softw Eng 29(5):417-429 · doi:10.1109/TSE.2003.1199071
[28] Prowell, SJ; Swain, WT, Sequence-based specification of critical software systems, Columbus, OH
[29] Prowell SJ, Trammell CJ, Linger RC, Poore JH (1999) Cleanroom software engineering: technology and process. Addison-Wesley, Reading
[30] SOS (2012) Satellite operations software enumeration. http://sqrl.eecs.utk.edu/btw/files/SOS_sr.html. Accessed 4 January 2013
[31] Swain WT (2011) Application of hybrid sequence-based specification to a data acquisition processor, Technical report UT-CS-11-669, University of Tennessee, Knoxville. http://sqrl.eecs.utk.edu/btw/files/WIM-HSBS-TR.pdf · Zbl 0568.68024
[32] Wang, Y.; Parnas, DL, Simulating the behavior of software modules by trace rewriting, Baltimore, MD
[33] Wang Y, Parnas DL (1994) Simulating the behavior of software modules by trace rewriting. IEEE Trans Softw Eng 20(10):750-759 · doi:10.1109/32.328996
[34] Weigh-In-Motion (2006) Weigh-In-Motion, cube management, and marking user manual. Oak Ridge National Laboratory, Oak Ridge, TN, Version 0.8.2 · Zbl 0225.94044
[35] WIMDAP (2012) Weigh-In-Motion data acquisition processor enumeration. http://sqrl.eecs.utk.edu/btw/files/WIMDAP_sr.html. Accessed 4 January 2013
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.