Abstract
With the increasing demand for highly dependable and constantly available systems, being able to reason about faults and their impact on systems is gaining considerable attention. In this paper, we are concerned with the provision of a logic especially tailored for describing fault tolerance properties, and supporting automated verification. This logic, which we refer to as dCTL, employs temporal deontic operators in order to distinguish “good” (normal) from “bad” (faulty) behaviors, using deontic permission, prohibition and obligation combined in a novel way with temporal operators. These formulas are interpreted over transition systems, in which normal executions are distinguished from faulty ones. Furthermore, we show that this logic is sufficiently expressive to describe various common properties of interest in fault tolerant systems, and show that it features some desirable characteristics that make it suitable for analysis. Indeed, even though we show that the logic is more expressive than CTL, we prove that it maintains the time complexity of the model checking problem for CTL. The logic, its expressiveness and its use to express properties of fault tolerant systems, are illustrated via some case studies.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Arora, A., Gouda, M.: Closure and Convergence: A Foundation of Fault-Tolerant Computing. IEEE Transactions on Software Engineering 19(11) (1999)
Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Castro, P., Maibaum, T.: Deontic Action Logic, Atomic Boolean Algebras and Fault-Tolerance. Journal of Applied Logic 7(4) (2009)
Clarke, E., Draghicescu, I.: Expressibility Results for Linear Time and Branching Time Logic. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1989)
Clarke, E., Emerson, E., Sistla, A.: Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2) (1986)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
Coenen, J.: Specifying Fault Tolerant Programs in Deontic Logic, Computing Science Notes 91/34, Dept. of Mathematics and Computing Science, Eindhoven University of Technology, Eindhoven, The Netherlands (1991)
D’Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of Live Behaviour Models for Fallible Domains. In: Proc. of International Conference on Software Engineering ICSE 2011. IEEE Press, Los Alamitos (2011)
Emerson, E., Halpern, J.: “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic. J. ACM 33(1) (1986)
French, T., McCabe-Dansted, J., Reynolds, M.: A Temporal Logic of Robustness. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 193–205. Springer, Heidelberg (2007)
Gnesi, E., Lenzini, G., Martinelli, F.: Logical Specification and Analysis of Fault Tolerant Systems through Partial Model Checking. Electronic Notes on Theoretical Computer Science, vol. 118. Elsevier, Amsterdam (2005)
Janowski, T.: On Bisimulation, Fault-Monotonicity and Provable Fault-Tolerance. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 292–306. Springer, Heidelberg (1997)
Magee, J., Maibaum, T.: Towards Specification, Modelling and Analysis of Fault Tolerance in Self Managed Systems. In: Proc. of International Workshop on Self-Adaptation and Self-Managing Systems SEAMS 2006. ACM Press, New York (2006)
McCabe-Dansted, J., French, T., Reynolds, M., Pinchinat, S.: On the Expressivity of RoCTL*. In: Proc. of the 16th International Symposium on Temporal Representation and Reasoning TIME 2009. IEEE Computer Society, Los Alamitos (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Castro, P.F., Kilmurray, C., Acosta, A., Aguirre, N. (2011). dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)