Skip to main content
SpringerLink
Log in

Rigorous Fault Tolerance Using Aspects and Formal Methods

  • Chapter
Rigorous Development of Complex Fault-Tolerant Systems

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4157))

  • 463 Accesses

Abstract

This paper examines the hypothesis that rigorous fault tolerance can be achieved by using aspect oriented software development in conjunction with formal methods of verification and analysis. After brief summaries on fault tolerance, aspect-oriented programming, and formal methods, some examples of aspects for fault tolerance are outlined. Then some recent research on applying formal methods to aspects is described, with the potential implications for rigorous fault tolerance using aspects.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arajo, J., Whittle, J., Kim, D.: Modeling and composing scenario-based requirements with aspects. In: The 12th IEEE International Requirements Engineering Conference (RE 2004), Kyoto, Japan, pp. 58–67 (September 2004)

    Google Scholar 

  2. Attiya, H., Welch, J.: Distributed Computing. McGraw-Hill Publishing Company, New York (1998)

    Google Scholar 

  3. Back, R., Sere, K.: Superposition refinement for reactive systems. Formal Aspects of Computing 8, 324–346 (1996)

    Article  MATH  Google Scholar 

  4. Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S., Ustuner, A.: Thorough static analysis of device drivers. In: Proceedings of EuroSys 2006, pp. 73–85. ACM, New York (2006)

    Chapter  Google Scholar 

  5. Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Balzarotti, D., D’Ursi, A., Cavallaro, L., Monga, M.: Slicing aspectj woven code. In: Proc. of Foundations of Aspect Languages Workshop (FOAL 2005) (2005)

    Google Scholar 

  7. Bhatti, N., Hiltunen, M., Schlichting, R., Chiu, W.: Coyote: A system for constructing fine-grain configurable communication services. ACM Transactions on Computer Systems 16(4), 321–366 (1998)

    Article  Google Scholar 

  8. Chandy, K.M., Lamport, L.: Distributed snapshots: determining global states of distributed systems. ACM Transactions on Computer Systems 3(1), 63–75 (1985)

    Article  Google Scholar 

  9. Chandy, K.M., Ramamoorthy, C.V.: Rollback and recovery strategies for computer programs. IEEE Transactions on Computers 21(6), 546–556 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  10. Chitchyan, R., Rashid, A., et al.: Report synthesizing state-of-the-art in aspect-oriented requirements engineering, architectures and design. In: AOSD-Europe research report AOSD-Europe-ULANC-9, pp. 1–259 (2005), available at: http://www.aosd-europe.net

  11. Clarke, S.: Extending standard UML with model composition semantics. Science of Computer Programming 44(1), 71–100 (2002)

    Article  MATH  Google Scholar 

  12. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  13. Clifton, C., Leavens, G.: Observers and assistants: a proposal for modular aspect-oriented reasoning. In: Foundations of Aspect Languages (FOAL), 2002. also, modified as Spectators and assistants: enabling modular aspect-oriented reasoning, Iowa State TR02-10 (2002)

    Google Scholar 

  14. Devereux, B.: Compositional reasoning about aspects using alternating-time logic. In: Proc. of Foundations of Aspect Languages Workshop (FOAL 2003) (2003)

    Google Scholar 

  15. Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  16. Douence, R., Fradet, P., Sudholt, M.: Composition, reuse, and interaction analysis of stateful aspects. In: Proc. of 3rd Intl. Conf. on Aspect-Oriented Software Development (AOSD 2004), pp. 141–150. ACM Press, New York (2004)

    Chapter  Google Scholar 

  17. Dror, E., Katz, S.: The architecture of the CAPE. Technical Report AOSD-Europe-Technion-4, AOSD-Europe (February 2006), available at: http://www.aosd-europe.net

  18. Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty processor. Journal of the ACM (JACM) 32, 374–382 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  19. Goldman, M., Katz, S.: Modular generic verification of LTL properties for aspects. In: Proc. of Foundations of Aspect Languages Workshop (FOAL 2006) (2006)

    Google Scholar 

  20. Hatcliff, J., Dwyer, M.B.: Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 39–58. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT) 2(4) (April 2000)

    Google Scholar 

  22. Hiltunen, M., Schlichting, R., Han, X., Cardozo, M., Das, R.: Real-time dependable channels: Customizing QoS attributes for distributed systems. IEEE Transactions on Parallel and Distributed Systems 10(6), 600–612 (1999)

    Article  Google Scholar 

  23. Hiltunen, M., Taiani, F., Schlichting, R.: Reflections on aspects and configurable protocols. In: Proc. of 5th Intl. Conf. on Aspect-Oriented Software Development (AOSD 2006), pp. 87–98. ACM Press, New York (2006)

    Chapter  Google Scholar 

  24. Holzmann, G.J., Peled, D.: The state of SPIN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 385–389. Springer, Heidelberg (1996)

    Google Scholar 

  25. Hutchinson, H., Peterson, L.: The x-kernel: an architecture for implementing network protocols. IEEE Transactions on Software Engineering 17(1), 64–76 (1991)

    Article  Google Scholar 

  26. Jalote, P.: Fault Tolerance in Distributed Systems. Prentice-Hall, Englewood Cliffs (1994)

    Google Scholar 

  27. Katara, M., Katz, S.: Architectural views of aspects. In: Proc. of 2nd Intl. Conf. on Aspect-Oriented Software Development (AOSD 2003), pp. 1–10 (2003)

    Google Scholar 

  28. Katz, E., Katz, S.: Verifying scenario-based aspect specifications. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 432–447. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  29. Katz, S.: A superimposition control construct for distributed systems. ACM Transactions on Programming Languages and Systems (TOPLAS) 15, 337–356 (1993)

    Article  Google Scholar 

  30. Katz, S.: Aspect categories and classes of temporal properties. In: Rashid, A., Aksit, M. (eds.) Transactions on Aspect-Oriented Software Development I. LNCS, vol. 3880, pp. 106–134. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  31. Katz, S., Perry, K.: Self-stabilizing extensions for message-passing systems. Distributed Computing 7, 17–26 (1993)

    Article  Google Scholar 

  32. Katz, S., Sihman, M.: Aspect validation using model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 373–394. Springer, Heidelberg (2004)

    Google Scholar 

  33. Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of aspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  34. Kienzle, J., Gelineau, S.: Ao challenge–implementing the ACID properties for transactional objects. In: Proceedings of 5th Intl. Conference on Aspect-Oriented Software Development (AOSD 2006), pp. 202–213 (2006)

    Google Scholar 

  35. Krishnamurthi, S., Fisler, K., Greenberg, M.: Verifying aspect advice modularly. In: Roy, B., Meier, W. (eds.) FSE 2004. LNCS, vol. 3017, pp. 137–146. Springer, Heidelberg (2004)

    Google Scholar 

  36. Lamport, L.: Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems 5(2), 190–222 (1983)

    Article  MATH  Google Scholar 

  37. Laprie, J.C.: Dependability: Basic Concepts and Terminology –in English, French, German, and Japanese. Series on Dependable Computing and Fault Tolerance, vol. 5. Springer, Heidelberg (1992)

    Google Scholar 

  38. Laprie, J.C., Arlat, J., Beounes, C., Kanoun, K., Hourtolle, C.: Hardware and software fault-tolerance: definition and analysis of architectural solutions. In: FTCS-17, pp. 116–121 ( June 1987)

    Google Scholar 

  39. Lee, P.A., Anderson, T.: Fault Tolerance: Principles and Practice, 2nd edn. Springer, Heidelberg (1990)

    MATH  Google Scholar 

  40. McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)

    Google Scholar 

  41. Mezini, M., Ostermann, K.: Conquering aspects with Ceasar. In: Proceedings of 2nd Intl. Conference on Aspect-Oriented Software Development (AOSD), pp. 90–99 (2003)

    Google Scholar 

  42. Nagy, I., Bergmans, L., Aksit, M.: Declarative aspect composition. In: Software Engineering Properties of Languages and Aspect Technologies (SPLAT) Workshop associated with AOSD 2004 (2004)

    Google Scholar 

  43. Ossher, H., Tarr, P.: Multi-dimensional separation of concerns and the hyperspace approach. In: Aksit, M. (ed.) Software Architectures and Component Technology. Kluwer Academic, Dordrecht (2001)

    Google Scholar 

  44. Pawlak, R., Duchien, L., Seinturier, L.: CompAr: Ensuring safe around advice composition. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 163–178. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  45. Pradhan, D.K., Vaidya, N.H.: Roll-forward checkpointing scheme: a novel fault-tolerant architecture. IEEE Transactions on Computers 43(10), 1163–1174 (1994)

    Article  MATH  Google Scholar 

  46. Rinard, M., Salcianu, A., Bugrara, S.: A classification system and analysis for aspect-oriented programs. In: Roy, B., Meier, W. (eds.) FSE 2004. LNCS, vol. 3017. Springer, Heidelberg (2004)

    Google Scholar 

  47. Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering 24(9), 709–720 (1998)

    Article  Google Scholar 

  48. Sereni, D., de Moor, O.: Static analysis of aspects. In: AOSD, pp. 30–39 (2003)

    Google Scholar 

  49. Sihman, M., Katz, S.: A calculus of superimpositions for distributed systems. In: Proc. of 1st Intl. Conf. on Aspect-Oriented Software Development (AOSD 2002), pp. 28–40. ACM Press, New York (2002)

    Chapter  Google Scholar 

  50. Sihman, M., Katz, S.: Superimposition and aspect-oriented programming. BCS Computer Journal 46(5), 529–541 (2003)

    Article  MATH  Google Scholar 

  51. Sipma, H.: A formal model for cross-cutting modular transition systems. In: Proc. of Foundations of Aspect Languages Workshop (FOAL 2003) (2003)

    Google Scholar 

  52. Storzer, M., Krinke, J.: Interference analysis for aspectj. In: Proc. of Foundations of Aspect Languages Workshop (FOAL 2003) (2003)

    Google Scholar 

  53. Xie, T., Zhou, J.: A framework and tool supports for generating test inputs of AspectJ programs. In: Proc. of 5th Intl. Conf. on Aspect-Oriented Software Development (AOSD 2006), pp. 190–201. ACM Press, New York (2006)

    Chapter  Google Scholar 

  54. Xu, D., Xu, W.: State-based incremental testing of aspect-oriented programs. In: Proc. of 5th Intl. Conf. on Aspect-Oriented Software Development (AOSD 2006), pp. 180–189. ACM Press, New York (2006)

    Chapter  Google Scholar 

  55. Zhou, J.: Slicing aspect-oriented software. In: IEEE International Workshop on Programming Comprehension, pp. 251–260 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The Technion, Haifa, Israel

    Shmuel Katz

Authors
  1. Shmuel Katz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Southampton, United Kingdom

    Michael Butler

  2. School of Computing Science, Newcastle University, Newcastle upon Tyne, NE1 7RU, UK

    Cliff B. Jones

  3. Computer Science School, Newcastle University, UK

    Alexander Romanovsky

  4. Ã…bo Akademi University, Finland

    Elena Troubitsyna

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Katz, S. (2006). Rigorous Fault Tolerance Using Aspects and Formal Methods. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds) Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol 4157. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916246_12

Download citation

  • DOI: https://doi.org/10.1007/11916246_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-48265-9

  • Online ISBN: 978-3-540-48267-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation