A two-level temporal logic for evolving specifications. (English) Zbl 1043.68069
Traditional information system specifications are fixed: the rules of the system are frozen at specification time. In practice, most systems have to change their rules in unexpected ways during their lifetime. We present here a simple variant of a temporal logic that deals with specification evolution. It is a linear time temporal logic with two levels of time: intervals, interrupted by mutations (changes of rules), which compose lives of the system. We present a complete axiom system and complexity results, which show a large compatibility with classical linear temporal logic.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Boehm, B. W., Improving software productivity, Computer, 20, 9, 43-57 (1987) |
| [2] | Conrad, S.; Ramos, J.; Saake, G.; Sernadas, C., Evolving logical specification in information systems, (Chomicki, J.; Saake, G., Logics for Databases and Information Systems (1998), Kluwer Academic Publishers: Kluwer Academic Publishers Boston, MA), Chapter 7, pp. 199-228 · Zbl 0905.03014 |
| [3] | Conrad, S.; Saake, G., Extending temporal logic for capturing evolving behaviour, (Ras, Z. W.; Skowron, A., ISMIS. ISMIS, Lecture Notes in Comput. Sci., 1325 (1997), Springer: Springer Berlin), 60-71 |
| [4] | Dubois, E., ALBERT: A formal language and its supporting tools for requirements engineering, (Lecture Notes in Comput. Sci., 1382 (1998), Springer: Springer Berlin), 322 |
| [5] | Fiadeiro, J.; Maibaum, T., Sometimes “tomorrow” is “sometime”: Action refinement in a temporal logic of objects, (Gabbay, D.; Ohlbach, H., Temporal Logic. Temporal Logic, Lecture Notes in Artificial Intelligence, 827 (1994), Springer: Springer Berlin), 48-66 · Zbl 0949.68539 |
| [6] | Gabbay, D.; Hodkinson, I.; Reynolds, M., Temporal Logic (1994), Clarendon Press: Clarendon Press Oxford · Zbl 0921.03023 |
| [7] | Hall, J. A., Seven myths of formal methods, IEEE Software, 7, 5, 11-19 (1990) |
| [8] | Jungclaus, R.; Saake, G.; Hartmann, T.; Sernadas, C., TROLL—A language for object-oriented specification of information systems, ACM Trans. Inform. Syst., 14, 2, 175-211 (1996) |
| [9] | Lichtenstein, O.; Pnueli, A.; Zuck, L. D., The glory of the past, (Parikh, R., Logics of Programs. Logics of Programs, Lecture Notes in Comput. Sci., 193 (1985), Springer: Springer Berlin), 196-218 · Zbl 0586.68028 |
| [10] | Merz, S.; Kröger, F., Layers of temporal structures, Fund. Inform. (1991) |
| [11] | Montanari, A.; Peron, A.; Policriti, A., Theories of \(ω\)-layered metric temporal structures: Expressiveness and decidability, Logic J. IGPL, 7, 79-102 (1999) · Zbl 0920.03033 |
| [12] | Montanari, A.; Policriti, A., Decidability results for metric and layered temporal logics, Notre Dame J. Formal Logic, 37, 2, 260-282 (1996) · Zbl 0858.03018 |
| [13] | Pnueli, A., Specification and development of reactive systems, (Kugler, H.-J., Information Processing 86, IFIP (1986), North-Holland: North-Holland Amsterdam), 845-858 |
| [14] | Ramos, J.; Sernadas, A., A brief introduction to gnome, Research report (1995), Section of Computer Science, Department of Mathematics, Instituto Superior Técnico: Section of Computer Science, Department of Mathematics, Instituto Superior Técnico 1096 Lisboa, Portugal |
| [15] | Saake, G.; Sernadas, A.; Sernadas, C., Evolving object specifications, (Wieringa, R.; Feenstra, R., Information Systems—Correctness and Reusability. Selected Papers from the IS-CORE Workshop (1995), World Scientific Publishing: World Scientific Publishing Singapore), 84-99 · Zbl 1043.68069 |
| [16] | Schobbens, P.-Y.; Sernadas, A.; Sernadas, C.; Saake, G., A two-level temporal logic for evolving specifications, Technical report (1998), FUNDP and Instituto Superior Tecnico: FUNDP and Instituto Superior Tecnico Lisbon · Zbl 1043.68069 |
| [17] | Sernadas, A.; Costa, J. F.; Sernadas, C., An institution of object behaviour, (Ehrig, H.; Orejas, F., Recent Trends in Data Type Specification. Recent Trends in Data Type Specification, Lecture Notes in Comput. Sci., 785 (1994), Springer: Springer Berlin), 337-350 · Zbl 0941.03534 |
| [18] | Sernadas, A.; Sernadas, C.; Costa, J. F., Object specification logic, J. Logic Comput., 5, 5, 603-630 (1995), Available as Research Report since 1992 · Zbl 0829.03013 |
| [19] | Sernadas, A.; Sernadas, C.; Ehrich, H.-D., Object-oriented specification of databases: An algebraic approach, (Hammersley, P., Very Large Data Bases 87 (1987), Morgan and Kaufmann: Morgan and Kaufmann Los Altos, CA), 107-116 |
| [20] | Sistla, A. P.; Clarke, E. M., The complexity of propositional linear temporal logic, J. ACM, 32, 3, 733-749 (1985) · Zbl 0632.68034 |
| [21] | Türker, C.; Conrad, S.; Saake, G., Dynamically changing behavior: An agent-oriented view to modeling intelligent information systems, (Ras, Z. W.; Michalewicz, M., ISMIS. ISMIS, Lecture Notes in Comput. Sci., 1079 (1996), Springer: Springer Berlin), 572-581 |
| [22] | Weyrauch, R. W., Prologomena to a theory of mechanized formal reasoning, Artificial Intelligence, 13, 1-2, 133-170 (1980) · Zbl 0435.68070 |
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.
