Geodesic
Jolie Static Type Checker: a prototype
Modelirovanie i analiz informacionnyh sistem, Tome 24 (2017) no. 6, pp. 704-717.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: static analysis, Jolie programming language.
Mots-clés : microservice 
@article{MAIS_2017_24_6_a3,
     author = {D. de Carvalho and M. Mazzara and B. Mingela and L. Safina and A. Tchitchigin and N. Troshkov},
     title = {Jolie {Static} {Type} {Checker:} a prototype},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {704--717},
     publisher = {mathdoc},
     volume = {24},
     number = {6},
     year = {2017},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a3/}
}
TY  - JOUR
AU  - D. de Carvalho
AU  - M. Mazzara
AU  - B. Mingela
AU  - L. Safina
AU  - A. Tchitchigin
AU  - N. Troshkov
TI  - Jolie Static Type Checker: a prototype
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2017
SP  - 704
EP  - 717
VL  - 24
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a3/
LA  - en
ID  - MAIS_2017_24_6_a3
ER  - 
%0 Journal Article
%A D. de Carvalho
%A M. Mazzara
%A B. Mingela
%A L. Safina
%A A. Tchitchigin
%A N. Troshkov
%T Jolie Static Type Checker: a prototype
%J Modelirovanie i analiz informacionnyh sistem
%D 2017
%P 704-717
%V 24
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a3/
%G en
%F MAIS_2017_24_6_a3
D. de Carvalho; M. Mazzara; B. Mingela; L. Safina; A. Tchitchigin; N. Troshkov. Jolie Static Type Checker: a prototype. Modelirovanie i analiz informacionnyh sistem, Tome 24 (2017) no. 6, pp. 704-717. http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a3/

[1] Akentev E., Tchitchigin A., Safina L., Mazzara M., Verified type checker for Jolie programming language, arXiv: 1703.05186 [cs.PL]

[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 | DOI

[5] Dragoni N., Dustdar S., Larsen S. T., Mazzara M., Microservices: Migration of a Mission Critical System, arXiv: 1704.04173 [cs.SE]

[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, eds. Bertrand Meyer, Manuel Mazzara, Springer, 2017, 195–216 | DOI

[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 (PSI Conference Series, 11th edition), Lecture Notes in Computer Science, Springer, 2017 | DOI

[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, eds. Bertrand Meyer, Manuel Mazzara, Springer, 2017, 217–225 | DOI

[10] Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12 (1969), 576–583 | DOI | MR

[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) | Zbl

[13] Mazzara M., Towards Abstractions for Web Services Composition, Ph.D. Thesis, University of Bologna, 2006

[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 | DOI

[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., Marraffa 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, arXiv: 1610.01778 [cs.SE]

[18] Milner R., Communication and concurrency, Prentice Hall International (UK) Ltd., 1995

[19] Milner R., Communicating and Mobile Systems: The $\pi$-calculus, Cambridge University Press, 1999 | MR | Zbl

[20] Montesi F., Guidi C., Zavattaro G., “Service-Oriented Programming with Jolie”, Web Services Foundations, Springer, 2014, 81–107 | DOI | MR

[21] Moura de L., Bjørner N., “Z3: An Efficient 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 | DOI

[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 | DOI | Zbl

[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 | DOI

[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 | Zbl

[26] Rice H. G., “Classes of Recursively Enumerable Sets and Their Decision Problems”, Trans. Amer. Math. Soc., 74 (1953), 358–366 | DOI | MR | Zbl

[27] Rondon P. M., Kawaguci M., Jhala R., “Liquid Types”, SIGPLAN Not., 43:6 (2008), 159–169 | DOI

[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 | DOI

[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/