A Formal Framework for Developing High Assurance Event Driven Service-Oriented Systems

  • Manuel Peralta
  • Supratik Mukhpadhyay
  • Ramesh Bharadwaj


We present a formal framework for developing distributed service-oriented systems in an event-driven secure synchronous programming environment. More precisely, our framework is built on the top of a synchronous programming language called SOL (Secure Operations Language) that has (i) capabilities of handling service invocations asynchronously, (ii) strong typing to ensure enforcement of information flow and security policies, and (iii) the ability to deal with failures of components. Applications written in our framework can be verified using formal static checking techniques like theorem proving. The framework runs on top of the SINS (Secure Infrastructure for Networked Systems) infrastructure developed by at the Naval Research Laboratory.


Security Policy Naval Research Laboratory Monitor Variable Service Invocation Vital Data 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Amir, Y. and J. Stanton (1998). The Spread Wide Area Group Communication System. Baltimore, MD, The Johns Hopkins University.Google Scholar
  2. [2]
    Appel, A. W. (1992). Compiling with Continuations, Cambridge University Press.Google Scholar
  3. [3]
    Benveniste, A., P. Caspi, et al. (2003). “The synchronous languages 12 years later.” Proceedings of the IEEE 91(1): 64–83.CrossRefGoogle Scholar
  4. [4]
    Berry, G. and G. Gonthier (1992). “The Esterel synchronous programming language: Design, semantics, implementation.” Sci. of Computer Prog.19.Google Scholar
  5. [5]
    Bharadwaj, R. (2002). “Verifiable Middleware for Secure Agent Interoperability.” Proc1 Second Goddard IEEE Workshop on Formal Approaches to Agent–Based Systems (FAABS II).Google Scholar
  6. [6]
    Bharadwaj, R. and C. Heitmeyer (1999). “Model Checking Complete Requirements Specifications using abstraction.” Automated Softw. Engg.6(1).Google Scholar
  7. [7]
    Bharadwaj, R., S. Mukhopadhyay (2007). SOLj: A Domain-Specific Language (DSL) for Secure Service-based Systems. IEEE International Workshop on Future Trends in Distributed Computing Systems. Sedona, AZ, IEEE Computer Society:173–180.Google Scholar
  8. [8]
    Bharadwaj, R., S. Mukhopadhyay (2008). A Formal Approach for Developing High-Assurance Event-driven Service-Oriented Systems. COMPSAC 2004, Turku, Finland, IEEE Computer Society.Google Scholar
  9. [9]
    Bharadwaj, R. and S.Mukhopadhyay (2008). From synchrony to SINS, Utah State University.Google Scholar
  10. [10]
    Bharadwaj, R. and S. Sims (2000). “Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking.” Proc. 6thInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2000), ETAPS 2000.Google Scholar
  11. [11]
    Birman, K. P. (2005). Reliable Distributed Systems, Springer.Google Scholar
  12. [12]
    Chandy, K. M. (2004). Event Servers for Crisis Management. HIPC.Google Scholar
  13. [13]
    Dijkstra, E. W. (1976). A Discipline of Programming, Prentice-Hall.Google Scholar
  14. [14]
    Gay, D., P. Levis, et al. (2003). The nesC language: A holistic approach to networked embedded systems. PLDI:1–11.Google Scholar
  15. [15]
    Halbwachs, N. (1993). “Delay Analysis in Synchronous Programs.” the I nternational Conference on Computer-Aided-Verification 697: 333–346.Google Scholar
  16. [16]
    Halbwachs, N. (1993). Delay Analysis in Synchronous Programs. the International Conference on Computer-Aided-Verification, Springer-Verlag. 697:333–346.Google Scholar
  17. [17]
    Heitmeyer, C. L., R. D. Jeffords, et al. (1996). “Automated Consistency Checking of Requirements Specifications.” ACM Transactions on Software Engineering and Methodology 5(3): 231–261.CrossRefGoogle Scholar
  18. [18]
    Kahn, G. (1974). The Semantics of a Simple Language for Parallel Programming. IFIP Congress.Google Scholar
  19. [19]
    Lee, E. A. (2005). “Absolutely Positively on Time: What Would It Take?” Computer 38(7): 85–87.CrossRefGoogle Scholar
  20. [20]
    Luckham, D. (2005). The Power of Events, Addison Wesley.Google Scholar
  21. [21]
    N. Benton, L. C., and C. Fournet (2005). “Modern Concurrency Abstractions for C#.” ACM TOPLAS 26(5): 769–804.CrossRefGoogle Scholar
  22. [22]
    Newcomer, E. (2002). Understanding Web Services, Addison Wesley.Google Scholar
  23. [23]
    OMG. Retrieved 31st October, 2008, from
  24. [24]
    Talpin, J.-P., P. L. Guernic, et al. (2003). Polychrony for Formal Refinement-Checking in a System-Level Design Methodology. ACSD:9–19.Google Scholar
  25. [25]
    Tressler, E. (2002). Inter-Agent Protocol for Distributed SOL Processing. Washington, DC, Naval Research Laboratory.Google Scholar
  26. [26]
    Wadler, P. (1994). “Monads and Composable Continuations.” Lisp and Symbolic Computation 7(1): 39–56.CrossRefGoogle Scholar
  27. [27]
    Yau, S. S., S. Mukhopadhyay, et al. (2005). Specification, Analysis, and Implementation of Architectural Patterns for Dependable Software Systems. IEEE WORDS.Google Scholar

Copyright information

© Springer-Verlag US 2009

Authors and Affiliations

  • Manuel Peralta
    • 1
  • Supratik Mukhpadhyay
    • 1
  • Ramesh Bharadwaj
    • 2
  1. 1.Utah State UniversityLoganUSA
  2. 2.Utah State UniversityLoganUSA

Personalised recommendations