Preview

Труды Института системного программирования РАН

Расширенный поиск

Refinement типы для языка Jolie

https://doi.org/10.15514/ISPRAS-2016-28(2)-2

Полный текст:

Аннотация

Jolie - язык программирования для разработки микросервисов и на текущий момент является динамически проверяемым. В статье рассматривается возможность объединить динамическую и статическую проверку типов с помощью refinement типов, проверяемых SMT-решателем. Соединение этих двух аспектов делает возможным сценарий, когда статическая верификация внутренних сервисов и динамическая проверка (потенциально злонамеренных) внешних сервисов совместно снижают объёмы необходимого тестирования и увеличивают безопасность системы. Refinement типы хорошо известны применительно к числовым типам данных, алгебраическим типам данных и массивам. Они основываются на соответствующих SMT теориях. Недавно SMT-решатели получили поддержку теории строк и регулярных выражений. В статье описывается возможность применения этой теории к строковым refinement типам. Мы используем язык программирования Jolie чтобы продемонстрировать целесообразность и полезность такого расширения. В первую очередь, потому что Jolie уже содержит синтаксическое расширение для строковых refinement типов. Мы развиваем указанное расширение, предоставляя статическую проверку типов. Во-вторых, поскольку в области микросервисов значение улучшенной проверки строковых данных гораздо выше, так как большинство коммуникаций с внешними системами происходит по текстовым протоколам. Мы демонстрируем упрощённый, но реалистичный пример системы из области web-разработки. В пример преднамеренно внесена ошибка, показывая, как легко она ускользает от традиционной системы типов. Предложенное расширение целесообразно, поскольку оно не пропускает программу с ошибкой. Полноценное решение потребует доработки в части точности проверки и качества сообщений об ошибках.

Об авторах

Александр Чичигин
Университет Иннополис
Россия


Лариса Сафина
Университет Иннополис
Россия


Мохамед Эльвакиль
Университет Иннополис
Россия


Мануэль Маццара
Университет Иннополис
Россия


Фабрицио Монтези
Университет Иннополис
Россия


Виктор Ривера
Университет Иннополис
Россия


Список литературы

1. EU Project SENSORIA. Accessed April 2016. http://www.sensoria-ist.eu/.

2. Gist of SMT constraints for the example. Accessed April 2016. https://gist.github.com/gabriel-fallen/a04c33860e2157201fa8.

3. Jolie Programming Language. Accessed April 2016. http://www.jolie-lang.org/.

4. WS-BPEL OASIS Web Services Business Process Execution Language. accessed April 2016. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.html.

5. Power Query formula reference. Technical Report, August 2015.

6. Microsoft Research. Accessed April 2016. Z3. https://github.com/Z3Prover/z3.

7. Jesper Bengtson, Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement types for secure implementations. ACM Trans. Program. Lang. Syst., 33(2):8:1–8:45, February 2011.

8. Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David Langworthy. Semantic subtyping with an SMT solver. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, pages 105–116, New York, NY, USA, 2010. ACM.

9. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In POPL, pages 263–274, 2013.

10. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg, 2008. Springer-Verlag.

11. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. J. ACM, 52(3):365–473, May 2005.

12. Joshua Dunfield. A unified system of type refinements. PhD thesis, Air Force Research Laboratory, 2007.

13. Cormac Flanagan. Hybrid type checking. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’06, pages 245–256, New York, NY, USA, 2006. ACM.

14. Tim Freeman and Frank Pfenning. Refinement types for ML. SIGPLAN Not., 26(6):268–277, May 1991.

15. Claudio Guidi, Ivan Lanese, Fabrizio Montesi, and Gianluigi Zavattaro. Dynamic error handling in service oriented applications. Fundam. Inform., 95(1):73–102, 2009.

16. Claudio Guidi, Roberto Lucchi, Gianluigi Zavattaro, Nadia Busi, and Roberto Gorrieri. Sock: a calculus for service oriented computing. In ICSOC, volume 4294 of LNCS, pages 327–338. Springer, 2006.

17. Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N Freund, and Cormac Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report), 2006.

18. James Lewis and Martin Fowler. Microservices: a definition of this new architectural term. Accessed April 2016. http://martinfowler.com/articles/microservices.htm.

19. Roberto Lucchi and Manuel Mazzara. A pi-calculus based semantics for WS-BPEL. J. Log. Algebr. Program., 70(1):96–118, 2007.

20. Manuel Mazzara, Faisal Abouzaid, Nicola Dragoni, and Anirban Bhattacharyya. Toward design, modelling and analysis of dynamic workflow reconfigurations – A process algebra perspective. In Web Services and Formal Methods - 8th International Workshop, WS-FM, pages 64–78, 2011.

21. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1–40, 41–77, September 1992.

22. Fabrizio Montesi. JOLIE: a Service-oriented Programming Language. Master’s thesis, University of Bologna, 2010.

23. Fabrizio Montesi. Process-aware web programming with Jolie. In Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC ’13, pages 761–763, New York, NY, USA, 2013. ACM.

24. Fabrizio Montesi and Marco Carbone. Programming Services with Correlation Sets. In Proc. of Service-Oriented Computing - 9th International Conference, ICSOC, pages 125–141, 2011.

25. Fabrizio Montesi, Claudio Guidi, and Gianluigi Zavattaro. Service-oriented programming with jolie. In Web Services Foundations, pages 81–107. 2014.

26. J. M. Nielsen. A Type System for the Jolie Language. Master’s thesis, Technical University of Denmark, 2013.

27. Mila Dalla Preda, Saverio Giallorenzo, Ivan Lanese, Jacopo Mauro, and Maurizio Gabbrielli. AIOCJ: A choreographic framework for safe adaptive distributed applications. In Software Language Engineering - 7th International Conference, SLE 2014, Västerås, Sweden, September 15-16, 2014. Proceedings, pages 161–170, 2014.

28. Larisa Safina, Manuel Mazzara, Fabrizio Montesi, and Victor Rivera. Data-driven workflows for microservices (genericity in jolie). In Proc. of the 30th IEEE International Conference on Advanced Information Networking and Applications (AINA), 2016.


Для цитирования:


Чичигин А., Сафина Л., Эльвакиль М., Маццара М., Монтези Ф., Ривера В. Refinement типы для языка Jolie. Труды Института системного программирования РАН. 2016;28(2):33-44. https://doi.org/10.15514/ISPRAS-2016-28(2)-2

For citation:


Tchitchigin A., Safina L., Elwakil M., Mazzara M., Montesi F., Rivera V. Refinement Types in Jolie. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(2):33-44. https://doi.org/10.15514/ISPRAS-2016-28(2)-2

Просмотров: 123


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)