Jolie Static Type Checker: a Prototype
Daniel de Carvalho,
Manuel Mazzara,
Bogdan Mingela,
Larisa Safina,
Alexander Tchitchigin,
Nikolay Troshkov https://doi.org/10.18255/1818-1015-2017-6-704-717
Abstract
Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and the dynamic one checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis. The article is published in the authors’ wording.
About the Authors
Daniel de Carvalho
Innopolis University
Russian Federation
PhD
Russian Federation
PhD
Manuel Mazzara
Innopolis University
Russian Federation
PhD
Russian Federation
PhD
Bogdan Mingela
Innopolis University
Russian Federation
student
Russian Federation
student
Larisa Safina
Innopolis University
Russian Federation
researcher
Russian Federation
researcher
Alexander Tchitchigin
Typeable.io LLC
Russian Federation
Russian Federation
Nikolay Troshkov
Innopolis University
Russian Federation
student
Russian Federation
student
References
1. Akentev E., Tchitchigin A., Safina L., Mazzara M., “Verified type checker for Jolie programming language”, https://arxiv.org/pdf/1703.05186.pdf.
2. Bandura A., Kurilenko N., Mazzara M., Rivera V., Safina L., Tchitchigin A., “Jolie Community on the Rise”, 9th IEEE International Conference on Service-Oriented Computing and Applications, SOCA, 2016.
3. Barrett C., Stump A., Tinelli C., “The SMT-LIB Standard. Version 2.0”, Proceedings of the 8th international workshop on satisfiability modulo theories, Edinburgh, England, 2010.
4. Cardelli L., “Type Systems”, ACM Computing Surveys, 28 (1996), 263–264.
5. Dragoni N., Dustdar S., Larsen S. T., Mazzara M., “Microservices: Migration of a Mission Critical System”, https://arxiv.org/abs/1704.04173.
6. Dragoni N., Giallorenzo S., Lluch-Lafuente A., Mazzara M., Montesi F., Mustafin R., Safina L., “Microservices: yesterday, today, and tomorrow”, Present and Ulterior Software Engineering, ed. Bertrand Meyer, Manuel Mazzara, Springer, 2017, 195–216.
7. Dragoni N., Lanese I., Larsen S. T., Mazzara M., Mustafin R., Safina L., “Microservices: How To Make Your Application Scale”, A.P. Ershov Informatics Conference (the PSI Conference Series, 11th edition), Lecture Notes in Computer Science, Springer, 2017.
8. Gmehlich R., Grau K., Loesch F., Iliasov A., Jackson M., Mazzara M., “Towards a formalism-based toolkit for automotive applications”, 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE 2013), IEEE Computer Society, 2013, 36–42.
9. Guidi C., Lanese I., Mazzara M., Montesi F., “Microservices: a Language-based Approach”, Present and Ulterior Software Engineering, ed. Bertrand Meyer, Manuel Mazzara, Springer, 2017, 217–225.
10. Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12 (1969), 576–583.
11. Jhala R., “Liquid Haskell”, https://ucsd-progsys.github.io/liquidhaskell-blog/.
12. MacKenzie M. C., Laskey K., McCabe F., Brown P. F., Metz R., “Reference model for service oriented architecture 1.0”, OASIS Standard, 12 (2006).
13. Mazzara M., Towards Abstractions for Web Services Composition, Ph.D. Thesis, University of Bologna, 2006, http://www.informatica.unibo.it/it/ricerca/technical-report/ 2006/UBLCS-2006-08.
14. Mazzara M., Abouzaid F., Dragoni N., Bhattacharyya A., “Toward Design, Modelling and Analysis of Dynamic Workflow Reconfigurations – A Process Algebra Perspective”, Web Services and Formal Methods, 8th International Workshop, WS-FM 2011, Lecture Notes in Computer Science, 7176, 2011, 64–78.
15. Mazzara M., Abouzaid F., Dragoni N., Bhattacharyya A., “Design, Modelling and Analysis of a Workflow Reconfiguration”, Proceedings of the International Workshop on Petri Nets and Software Engineering, Newcastle upon Tyne, UK, June 20–21, 2011, 10–24.
16. Mazzara M., Biselli L., Greco P. P., Dragoni N., Marra˙a A., Qamar N., Simona de Nicola, “Social networks and collective intelligence: a return to the agora”, Social Network Engineering for Secure Web Data and Services, IGI Global, 2013.
17. Mazzara M., Mustafin R., Safina L., Lanese I., “Towards Microservices and Beyond: An incoming Paradigm Shift in Distributed Computing”, https://arxiv.org/pdf/1610. 01778.pdf.
18. Milner R., Communication and concurrency, Prentice Hall International (UK) Ltd., 1995.
19. Milner R., Communicating and Mobile Systems: The ˇ-calculus, Cambridge University Press, 1999.
20. Montesi F., Guidi C., Zavattaro G., “Service-Oriented Programming with Jolie”, Web Services Foundations, Springer, 2014, 81–107.
21. Moura de L., Bjørner N., “Z3: An E˚cient SMT Solver”, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008 (Budapest, Hungary, March 29–April 6, 2008), Lecture Notes in Computer Science, 4963, Springer, 2008, 337–340.
22. Moura de L., Bjørner N., “Satisfiability modulo theories: An appetizer”, Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Lecture Notes in Computer Science, 5902, Springer, 2009, 23–36.
23. Nalin M., Baroni I., Mazzara M., “A Holistic Infrastructure to Support Elderlies’ Independent Living”, Encyclopedia of E-Health and Telemedicine, IGI-Global, 2016, 591–605.
24. Newman S., Building microservices, O’Reilly Media, Inc., 2015.
25. Nielsen J. M., A Type System for the Jolie Language, Master thesis, Technical University of Denmark, 2013.
26. Rice H. G., “Classes of Recursively Enumerable Sets and Their Decision Problems”, Trans. Amer. Math. Soc., 74 (1953), 358–366.
27. Rondon P. M., Kawaguci M., Jhala R., “Liquid Types”, SIGPLAN Not., 43:6 (2008), 159– 169.
28. Safina L., Mazzara M., Montesi F., Rivera V., “Data-driven Workflows for Microservices (genericity in Jolie)”, Proc. of the 30th IEEE International Conference on Advanced Information Networking and Applications (AINA 2016), 2016.
29. Salikhov D., Khanda K., Gusmanov K., Mazzara M., Mavridis N., “Microservice-based IoT for Smart Buildings”, Proceedings of the 31st International Conference on Advanced Information Networking and Applications Workshops (WAINA), 2017.
30. Salikhov D., Khanda K., Gusmanov K., Mazzara M., Mavridis N., “Jolie Good Buildings: Internet of things for smart building infrastructure supporting concurrent apps utilizing distributed microservices”, Proceedings of the 1st International conference on Convergent Cognitive Information Technologies, 2016.
31. Tchitchigin A., Safina L., Mazzara M., Elwakil M., Montesi F., Rivera V., “Refinement types in Jolie”, Spring/Summer Young Researchers Colloquium on Software Engineering, SYRCoSE, 2016.
32. Vallverdú J., Talanov M., Distefano S., Mazzara M., Tchitchigin A., Nurgaliev I., “A cognitive architecture for the implementation of emotions in computing systems”, Biologically Inspired Cognitive Architectures, 15 (2016), 34 – 40.
33. “Z3”, https://github.com/Z3Prover/z3.
34. “OASIS. Web Services Business Process Execution Language”, http://docs.oasis-open. org/wsbpel/2.0/wsbpel-specification-draft.html.
35. “Agda”, http://wiki.portal.chalmers.se/agda/pmwiki.php.
36. “F*”, https://www.fstar-lang.org/.
Review
For citations:
de Carvalho D., Mazzara M., Mingela B., Safina L., Tchitchigin A., Troshkov N. Jolie Static Type Checker: a Prototype. Modeling and Analysis of Information Systems. 2017;24(6):704-717. https://doi.org/10.18255/1818-1015-2017-6-704-717
Views:
1290
Email this article 