Abstract
In order to reconcile the state of the art and the state of the practice in software engineering, immediate goals aim to use formal methods in ways that are minimally disruptive to professional practice. In this pursuit formal methods should be adapted to flexible lifecycle structures, getting over more traditional approaches. In the field of real-time design, SCTL/MUS-T methodology proposes a software process using formal methods that builds incrementally the model-oriented specification of the intended system. There are two main issues in this proposal: the incremental nature of the process, calling for a many-valued understanding of the world; and the construction of a model-oriented specification, calling for an imperative viewpoint in specification. From this starting point, this paper introduces a many-valued logic with imperative semantics enabling (1) to build a very-abstract level prototype from the scenarios identified on the intended system; (2) to capture the uncertainty and disagreement in an incremental process by providing a measure of how far or how close the prototype is from satisfying the intended requirements.
This work was partially supported by the Xunta de Galicia Basic Research Project PGIDT01PX132203PR.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Larsen, K.G., Steffen, B., Weise, C.: Continuous Modeling of Real-Time and Hybrid Systems: From Concepts to Tools. Intl. Journal on Software Tools for Technology Transfer 1, 64–85 (1997)
Alur, R.: Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Dept. of Computer Science, Stanford University (1991)
van Lamsweerde, A.: Formal Specification: a Roadmap. In: 22nd Intl. Conference on Software Engineering (ICSE 2000), pp. 147–159. ACM Press, New York (2000)
Chechik, M., Devereux, B., Easterbrook, S.M., Lai, A., Petrovykh, V.: Efficient Multiple-Valued Model-Checking Using Lattice Representations. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 441–455. Springer, Heidelberg (2001)
Alur, R., Henzinger, T.A.: Logics and Models of Real Time: A Survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)
Fernández Vilas, A., Pazos Arias, J.J., Díaz Redondo, R.P.: Extending Timed Automaton and Real-time Logic to Many-valued Reasoning. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 185–204. Springer, Heidelberg (2002)
Fernández Vilas, A., Pazos Arias, J.J., Gil Solla, A., Díaz Redondo, R.P., García Duque, J., Barragáns Martínez, A.B.: Incremental Specification with SCTL/MUST: a Case Study. The Journal of Systems & Software 71(2) (2004) (to appear)
Alur, R., Courcoubetis, C., Dill, D.: Model Checking in Dense Real-time. Information and Computation 104, 2–34 (1993)
Pazos Arias, J.J., García Duque, J.: SCTL-MUS: A Formal Methodology for Software Development of Distributed Systems. A Case Study, Formal Aspects of Computing 13, 50–91 (2001)
Barringer, H., Fisher, M., Gabbay, D., Gough, G., Owens, R.: METATEM: An Introduction. Formal Aspects of Computing 7, 533–549 (1995)
Merz, S.: Efficiently Executable Temporal Logic Programs. In: Fisher, M., Owens, R. (eds.) IJCAI-WS 1993. LNCS, vol. 897, pp. 69–85. Springer, Heidelberg (1995)
Laroussinie, F., Larsen, K.G., Weise, C.: From Timed Automata to Logic - And Back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995)
Tripakis, S., Yovine, S.: Analysis of Timed Systems using Time-abstracting Bisimulations. Formal Methods in System Design 18, 25–68 (2001)
Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed Modal Specifications – Theory and Tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993)
Harel, D., Kugler, H.: Synthesizing Sate-based Object Systems from LSC Specifications. Intl. Journal of Foundations of Computer Science 13, 5–51 (2002)
Harel, D., Marelly, R.: Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In: 10th Intl. Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2002), pp. 193–202. IEEE Computer Society Press, Los Alamitos (2002)
Fisher, M., Owens, R. (eds.): IJCAI-WS 1993. LNCS, vol. 897. Springer, Heidelberg (1995)
Altisen, K., Goessler, G., Sifakis, J.: Scheduler Modeling Based on the Controller Synthesis Paradigm. Real-Time Systems 23, 55–84 (2002)
Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)
Konikowska, B., Penczek, W.: Model Checking for Multi-Valued CTL*. In: Beyond Two: Theory and Applications of Multiple-valued Logic, pp. 193–210. Springer, Heidelberg (2003)
van Lamsweerde, A., Willemet, L.: Inferring Declarative Requirements Specifications from Operational Scenarios. IEEE Transactions on Software Engineering, Special Issue on Scenario Management 24, 1089–1114 (1998)
Moser, L.E., Ramakrishna, Y.S., Kutty, G., Melliar Smith, P.M., Dillon, L.K.: A Graphical Environment for Design of Concurrent Real-Time Systems. ACM Transactions on Software Engineering and Methodology 6, 31–79 (1997)
Barragáns Martínez, A.B., García Duque, J., Pazos Arias, J.J., Fernández Vilas, A., Díaz Redondo, R.P.: Requirements Specification Evolution in a Multi-Perspective Environment. In: 26th Annual Intl. Conference on Computer Software and Applications (COMPSAC 2002), pp. 39–44. IEEE Computer Society Press, Los Alamitos (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vilas, A.F., Arias, J.J.P., Redondo, R.P.D., Solla, A.G., Duque, J.G. (2004). A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-24756-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21377-2
Online ISBN: 978-3-540-24756-2
eBook Packages: Springer Book Archive