INVESTIGADORES
FRIAS Marcelo Fabian
artículos
Título:
Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy
Autor/es:
AGUIRRE, NAZARENO; FRIAS, MARCELO FABIAN; MOSCATO, MARIANO MIGUEL; MAIBAUM, THOMAS STEPHEN EDWARD; WASSYNG ALAN
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer
Referencias:
Año: 2009 vol. 5503 p. 155 - 170
ISSN:
0302-9743
Resumen:
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.