Developing Honest Java Programs with Diogenes

  • Nicola Atzei
  • Massimo BartolettiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)


Modern distributed applications are typically obtained by integrating new code with legacy (and possibly untrusted) third-party services. Some recent works have proposed to discipline the interaction among these services through behavioural contracts. The idea is a dynamic discovery and composition of services, where only those with compliant contracts can interact, and their execution is monitored to detect and sanction contract breaches. In this setting, a service is said honest if it always respects the contracts it advertises. Being honest is crucial, because it guarantees a service not to be sanctioned; further, compositions of honest services are deadlock-free. However, developing honest programs is not an easy task, because contracts must be respected even in the presence of failures (whether accidental or malicious) of the context. In this paper we present Diogenes, a suite of tools which supports programmers in writing honest Java programs. Through an Eclipse plugin, programmers can write a specification of the service, verify its honesty, and translate it into a skeletal Java program. Then, they can refine this skeleton into proper Java code, and use the tool to verify that its honesty has not been compromised by the refinement.


Model Checker Order Amount Java Program Online Store Abstract Semantic 
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.



This work has been partially supported by Aut. Reg. of Sardinia P.I.A. 2013 “NOMAD”, and by EU COST Action IC1201 “Behavioural Types for Reliable Large-Scale Software Systems” (BETTY).


  1. 1.
    van der Aalst, W.M.P., Lohmann, N., Massuthe, P., Stahl, C., Wolf, K.: Multiparty contracts: agreeing and implementing interorganizational processes. Comput. J. 53(1), 90–106 (2010)CrossRefGoogle Scholar
  2. 2.
    Acciai, L., Boreale, M., Zavattaro, G.: Behavioural contracts with request-response operations. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 16–30. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Barbanera, F., de’Liguoro, U.: Two notions of sub-behaviour for session-based client/server systems. In: PPDP, pp. 155–164. ACM (2010)Google Scholar
  4. 4.
    Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: Compliance and subtyping in timed session types. In: Graf, S., Viswanathan, M. (eds.) Formal Techniques for Distributed Objects, Components, and Systems. LNCS, vol. 9039, pp. 161–177. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  5. 5.
    Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: A contract-oriented middleware. In: Braga, C., et al. (eds.) FACS 2015. LNCS, vol. 9539, pp. 86–104. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-28934-2_5. CrossRefGoogle Scholar
  6. 6.
    Bartoletti, M., Murgia, M., Scalas, A., Zunino, R.: Verifiable abstractions for contract-oriented systems. JLAMP (2015, to appear)Google Scholar
  7. 7.
    Bartoletti, M., Scalas, A., Tuosto, E., Zunino, R.: Honesty by typing. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 305–320. Springer, Heidelberg (2013). CrossRefGoogle Scholar
  8. 8.
    Bartoletti, M., Tuosto, E., Zunino, R.: Contract-oriented computing in \({\rm CO}_2\). Sci. Ann. Comp. Sci. 22(1), 5–60 (2012)MathSciNetGoogle Scholar
  9. 9.
    Bartoletti, M., Zunino, R.: On the decidability of honesty and of its variants. In: Hildebrandt, T., Ravara, A., van der Werf, J.M., Weidlich, M. (eds.) WS-FM 2014 + WS-FM 2015. LNCS, vol. 9421, pp. 143–166. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-33612-1_9 CrossRefGoogle Scholar
  10. 10.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. In: TCS (2001)Google Scholar
  11. 11.
  12. 12.
    Eker, S., Meseguer, J., Sridharanarayanan, A.: The maude LTL model checker. Electr. Notes Theor. Comput. Sci. 71, 162–187 (2002)CrossRefzbMATHGoogle Scholar
  13. 13.
  14. 14.
    Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)Google Scholar
  15. 15.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  16. 16.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1–9:67 (2016)CrossRefzbMATHGoogle Scholar
  17. 17.
    Laneve, C., Padovani, L.: The must preorder revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 80–102. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Mukhija, A., Dingwall-Smith, A., Rosenblum, D.: QoS-aware service composition in Dino. In: ECOWS, LNCS, vol. 5900, pp. 3–12. Springer (2007)Google Scholar
  20. 20.
    Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  1. 1.Università Degli Studi di CagliariCagliariItaly

Personalised recommendations