Artículo
Abstract:
We propose complementing tabular notations used in requirements specifications, such as those used in the SCR method, with a formalism for describing specific, useful, subclasses of computations, i.e., particular combinations of the atomic transitions specified within tables. This provides the specifier with the ability of driving the execution of transitions specified by tables, without the onerous burden of having to introduce modifications into the tabular expressions; thus, it avoids the problem of modifying the object of analysis, which would make the analysis indirect and potentially confusing. This is useful for a number of activities, such as defining test harnesses for tables, and concentrating the analyses on particular, interesting, subsets of computations. Unlike previous approaches, ours allows for the description of a wider class of combinations of the transitions defined by tables, by means of a rich operational language. This language is an extension of the Alloy language, called DynAlloy, whose notation is inspired by that of dynamic logic. The use of DynAlloy enables us to provide an extra mechanism for the analysis of tabular specifications, based on SAT solving. We will illustrate this and the features of our approach via an example based on a known tabular specification of a simple autopilot system.
Registro:
| Documento: | Artículo |
| Título: | Describing and analyzing behaviours over tabular specifications using (Dyn)alloy |
| Autor: | Aguirre, N.M.; Frias, M.F.; Moscato, M.M.; Maibaum, T.S.E.; Wassyng, A. |
| Filiación: | Department of Computer Science, FCEFQyN, Universidad Nacional de Rio Cuarto and CONICET, Argentina Department of Computer Science, FCEyN, Universidad de Buenos Aires and CONICET, Argentina Department of Computing and Software, McMaster University, Canada |
| Palabras clave: | Atomic transition; Autopilot systems; Dynamic logic; Example based; Operational languages; Requirements specifications; SAT-solving; Tabular expressions; Tabular notation; Tabular specifications; Test harness; Alloy languages; Atomic transition; Autopilot systems; Operational languages; Requirements specifications; Tabular expressions; Tabular notation; Tabular specifications; Computer software; Linguistics; Specifications; Specifications; Cerium alloys; Software engineering |
| Año: | 2009 |
| Volumen: | 5503 |
| Página de inicio: | 155 |
| Página de fin: | 170 |
| DOI: | http://dx.doi.org/10.1007/978-3-642-00593-0_11 |
| Título revista: | 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/paper/paper_03029743_v5503_n_p155_Aguirre.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5503_n_p155_Aguirre |
Referencias:
- Bharadwaj, R., Heitmeyer, C., Applying the SCR Requirements Specification Method to Practical Systems: A Case Study (1996) 21st Software Engineering Workshop, NASA GSFC
- Bharadwaj, R., Heitmeyer, C., Applying the SCR Requirements Method to a Simple Autopilot (1997) Proc. of the Fourth NASA Langley Formal Methods Workshop
- Bultan, T., Heitmeyer, C., Analyzing Tabular Requirements Specifications using Infinite State Model Checking (2006) Proc. of MEMOCODE 2006
- Frias, M., Galeotti, J.P., López Pombo, C., Aguirre, N., DynAlloy: Upgrading alloy with actions (2005) Proc. of ICSE 2005, , ACM Press, New York
- Gargantini, A., Heitmeyer, C., Using Model Checking to Generate Tests from Requirements Specifications (1999) ESEC 1999 and ESEC-FSE 1999. LNCS, 1687. , Nierstrasz, O., Lemoine, M. (eds.) Springer, Heidelberg
- Heitmeyer, C., Bull, A., Gasarch, C., Labaw, B., SCR*: A Toolset for Specifying and Analyzing Requirements (1996) Abstract Data Types 1995 and COMPASS 1995. LNCS, 1130. , In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Springer, Heidelberg
- Heitmeyer, C., Jeffords, R., Labaw, B., Automated consistency checking of requirements specifications (1996) ACM Trans. on Soft. Eng. and Methodology, 5 (3)
- Heitmeyer, C., Archer, M., Bharadwaj, R., Jeffords, R., Tools for constructing requirements specifications: The SCR Toolset at the age of nine (2005) Computer Systems: Science & Engineering, 20 (1)
- Heninger, K., Kallander, J., Parnas, D., Shore, J., Software Requirements for the A-7E Aircraft (1978) NLR Memorandum Report 3876, US Naval Research Lab
- Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Trans. on Soft. Eng. and Methodology, 11 (2)
- Jackson, D., Software abstractions (2006) Logic, Language, and Analysis, , MIT Press, Cambridge
- Leveson, N., Heimdahl, M., Hildreth, H., Reese, J., Requirements Specifications for Process-Control Systems (1994) IEEE Trans. on Software Engineering, 20 (9)
- Owre, S., Rushby, J., Shankar, N., Analyzing Tabular and State-Transition Specifications in PVS (1997) TACAS 1997. LNCS, 1217. , In: Brinksma, E. (ed.) Springer, Heidelberg
Citas:
---------- APA ----------
Aguirre, N.M., Frias, M.F., Moscato, M.M., Maibaum, T.S.E. & Wassyng, A. (2009) . Describing and analyzing behaviours over tabular specifications using (Dyn)alloy. 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009, 5503, 155-170.http://dx.doi.org/10.1007/978-3-642-00593-0_11
---------- CHICAGO ----------
Aguirre, N.M., Frias, M.F., Moscato, M.M., Maibaum, T.S.E., Wassyng, A. "Describing and analyzing behaviours over tabular specifications using (Dyn)alloy" . 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009 5503 (2009) : 155-170.http://dx.doi.org/10.1007/978-3-642-00593-0_11
---------- MLA ----------
Aguirre, N.M., Frias, M.F., Moscato, M.M., Maibaum, T.S.E., Wassyng, A. "Describing and analyzing behaviours over tabular specifications using (Dyn)alloy" . 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009, vol. 5503, 2009, pp. 155-170.http://dx.doi.org/10.1007/978-3-642-00593-0_11
---------- VANCOUVER ----------
Aguirre, N.M., Frias, M.F., Moscato, M.M., Maibaum, T.S.E., Wassyng, A. Describing and analyzing behaviours over tabular specifications using (Dyn)alloy. Lect. Notes Comput. Sci. 2009;5503:155-170.http://dx.doi.org/10.1007/978-3-642-00593-0_11
