Significant research efforts for the convergence of Web and Telecommunication services have been recently spent by research and industry stakeholders. The IETF and W3C are cooperating in specifying how web browsers should evolve to natively support communication services. In this perspective, devising novel mechanisms for the signaling message exchange and possible interworking between Web- and SIP- based systems is a hot topic of research. Indeed, discussions are still ongoing on how differences between REpresentational State Transfer (REST) and Session Initiation Protocol (SIP) models should be coped with. This issue is made more difficult by the lack of rigorous modeling of RESTful systems. In this article we propose a rigorous approach for the design and implementation of REST communication services (e.g., a call service) which leverages formal verification techniques, while while allowing to meet a specific performance requirement (i.e. maximum call setup delay). First, we formalize the call resource behavior through a Finite State Machine representation by modeling and simulating service expected behavior and its interworking with SIP User Agents through a tool for the analysis of communicating state machines. Then, we use the model-checking capabilities offered by the tool for the verification of formal properties. Finally, we implement a prototype that, thanks to the previous formalization step, is shown to be functionally correct, while yielding acceptable performance.

Formalizing REST APIs for web-based communication and SIP interworking / Paganelli, Federica; Ambra, Terence; Fantechi, Alessandro; Giuli, Dino. - In: TELECOMMUNICATION SYSTEMS. - ISSN 1018-4864. - STAMPA. - (2017), pp. 1-19. [10.1007/s11235-016-0271-2]

Formalizing REST APIs for web-based communication and SIP interworking

PAGANELLI, FEDERICA;AMBRA, TERENCE;FANTECHI, ALESSANDRO;GIULI, DINO
2017

Abstract

Significant research efforts for the convergence of Web and Telecommunication services have been recently spent by research and industry stakeholders. The IETF and W3C are cooperating in specifying how web browsers should evolve to natively support communication services. In this perspective, devising novel mechanisms for the signaling message exchange and possible interworking between Web- and SIP- based systems is a hot topic of research. Indeed, discussions are still ongoing on how differences between REpresentational State Transfer (REST) and Session Initiation Protocol (SIP) models should be coped with. This issue is made more difficult by the lack of rigorous modeling of RESTful systems. In this article we propose a rigorous approach for the design and implementation of REST communication services (e.g., a call service) which leverages formal verification techniques, while while allowing to meet a specific performance requirement (i.e. maximum call setup delay). First, we formalize the call resource behavior through a Finite State Machine representation by modeling and simulating service expected behavior and its interworking with SIP User Agents through a tool for the analysis of communicating state machines. Then, we use the model-checking capabilities offered by the tool for the verification of formal properties. Finally, we implement a prototype that, thanks to the previous formalization step, is shown to be functionally correct, while yielding acceptable performance.
2017
1
19
Paganelli, Federica; Ambra, Terence; Fantechi, Alessandro; Giuli, Dino
File in questo prodotto:
File Dimensione Formato  
Rest_telco_2017_author.pdf

Accesso chiuso

Descrizione: Articolo principale
Tipologia: Pdf editoriale (Version of record)
Licenza: Tutti i diritti riservati
Dimensione 1.36 MB
Formato Adobe PDF
1.36 MB Adobe PDF   Richiedi una copia

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1074828
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact