Davide Basile
ABSTRACT
Featured modal contract automata (FMCA) have been proposed as a suitable formalism for modelling contract-based dynamic service product lines. A contract is a behavioural description consisting of offers and necessary and permitted service requests with different levels of criticality, to be matched with corresponding offers of other FMCA. Each contract is equipped with a feature constraint, whose features are offers or requests, and characterises a valid product orchestration. A safe orchestration of a product fulfils all necessary and the maximum number of permitted requests, such that all enabled features are available and none of its disabled features is. The entire product line orchestration can be computed from a subset of valid product orchestrations, by exploiting their (partial) ordering. The open-source prototypical toolkit FMCAT supports the specification and orchestration of FMCA, and it interfaces with FeatureIDE for importing feature models and their valid products. In this experience report, we show how to model a Hotel service product line with FMCA and how to analyse it with FMCAT.
- K Bąk, Z. Diskin, M. Antkiewicz, K. Czarnecki, and A. Wąsowski. 2016. Clafer: unifying class and feature modeling. Softw. Syst. Model. 15, 3 (2016), 811--845. Google Scholar
Digital Library
- M. Bartoletti, T. Cimoli, and R. Zunino. 2015. Compliance in Behavioural Contracts: A Brief Survey. In Programming Languages with Applications to Biology and Security (LNCS), C. Bodei, G.L. Ferrari, and C. Priami (Eds.), Vol. 9465. Springer, 103--121.Google Scholar
- D. Basile, P. Degano, and G.L. Ferrari. 2016. Automata for Specifying and Orchestrating Service Contracts. Log. Meth. Comput. Sci. 12, 4:6 (2016), 1--51.Google Scholar
- D. Basile, F. Di Giandomenico, and S. Gnesi. 2017. FMCAT: Supporting Dynamic Service-based Product Lines. In Proceedings 21st International Systems and Software Product Line Conference (SPLC'17), M. ter Beek, W. Cazzola, O. Díaz, M. La Rosa, R.E. López-Herrejón, T. Thüm, J. Troya, A. Ruiz-Cortés, and D. Benavides (Eds.), Vol. 2. ACM, 3--8. Google ScholarDigital Library
- D. Basile, F. Di Giandomenico, S. Gnesi, P. Degano, and G.L. Ferrari. 2017. Specifying Variability in Service Contracts. In Proceedings 11th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS'17), M.H. ter Beek, N. Siegmund, and I. Schaefer (Eds.). ACM, 20--27. Google ScholarDigital Library
- D. Basile, M.H. ter Beek, F. Di Giandomenico, and S. Gnesi. 2017. Orchestration of Dynamic Service Product Lines with Featured Modal Contract Automata. In Proceedings 21st International Systems and Software Product Line Conference (SPLC'17), M. ter Beek, W. Cazzola, O. Díaz, M. La Rosa, R.E. López-Herrejón, T. Thüm, J. Troya, A. Ruiz-Cortés, and D. Benavides (Eds.), Vol. 2. ACM, 117--122. Google ScholarDigital Library
- D.S. Batory. 2005. Feature Models, Grammars, and Propositional Formulas. In Proceedings 9th International Software Product Lines Conference (SPLC'05) (LNCS), J.H. Obbink and K. Pohl (Eds.), Vol. 3714. Springer, 7--20. Google ScholarDigital Library
- M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. 2016. Towards a Feature mu-Calculus Targeting SPL Verification. In Proceedings 7th International Workshop on Formal Methods and Analysis for Software Product Line Engineering (FMSPLE'16) (EPTCS), J. Rubin and T. Thüm (Eds.), Vol. 206. Open Publishing Association, 61--75.Google Scholar
- M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. 2017. Family-Based Model Checking with mCRL2. In Proceedings 20th International Conference on Fundamental Approaches to Software Engineering (FASE'17) (LNCS), M. Huisman and J. Rubin (Eds.), Vol. 10202. Springer, 387--405. Google ScholarDigital Library
- M.H. ter Beek, S. Gnesi, and M.N. Njima. 2011. Product Lines for Service Oriented Applications - PL for SOA. In Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems (WWV'11) (EPTCS), L. Kovács, R. Pugliese, and F. Tiezzi (Eds.), Vol. 61. Open Publishing Association, 34--48.Google Scholar
- M.H. ter Beek, M.A. Reniers, and E.P. de Vink. 2016. Supervisory Controller Synthesis for Product Lines Using CIF 3. In Proceedings 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA'16) (LNCS), T. Margaria and B. Steffen (Eds.), Vol. 9952. Springer, 856--873.Google ScholarCross Ref
- D.A. van Beek, W.J. Fokkink, D. Hendriks, A. Hofkamp, J. Markovski, J.M. van de Mortel-Fronczak, and M.A. Reniers. 2014. CIF 3: Model-Based Engineering of Supervisory Controllers. In Proceedings 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14) (LNCS), E. Ábrahám and K. Havelund (Eds.), Vol. 8413. Springer, 575--580.Google Scholar
- G. Behrmann, A. David, K.G. Larsen, J. Håkansson, P. Pettersson, W. Yi, and M. Hendriks. 2006. UPPAAL 4.0. In Proceedings 3rd International Conference on the Quantitative Evaluation of SysTems (QEST'06). IEEE, 125--126. Google ScholarDigital Library
- A. Bouguettaya, M. Singh, M. Huhns, Q.Z. Sheng, H. Dong, Q. Yu, A.G. Neiat, S. Mistry, B. Benatallah, B. Medjahed, M. Ouzzani, F. Casati, X. Liu, H. Wang, D. Georgakopoulos, L. Chen, S. Nepal, Z. Malik, A. Erradi, Y. Wang, B. Blake, S. Dustdar, F. Leymann, and M. Papazoglou. 2017. A Service Computing Manifesto: The Next 10 Years. Commun. ACM 60, 4 (April 2017), 64--72. Google ScholarDigital Library
- C.G. Cassandras and S. Lafortune. 2006. Introduction to Discrete Event Systems. Springer, New York, NY, USA. Google ScholarDigital Library
- A. Classen, M. Cordy, P.-Y. Schobbens, P. Heymans, A. Legay, and J.-F. Raskin. 2013. Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Softw. Eng. 39, 8 (2013), 1069--1089. Google ScholarDigital Library
- G. Cledou and L. Barbosa. 2017. Modeling Families of Public Licensing Services: A Case Study. In Proceedings 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE'17), S. Gnesi, N. Plat, and H. Melgratti (Eds.). ACM, 37--43. Google ScholarDigital Library
- S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, W. Wesselink, and T.A.C. Willemse. 2013. An Overview of the mCRL2 Toolset and Its Recent Advances. In Proceedings 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13) (LNCS), N. Piterman and S.A. Smolka (Eds.), Vol. 7795. Springer, 199--213. Google ScholarDigital Library
- A. David et al. 2017. UPPAAL DBM Library. Retrieved Nov 1, 2017 from http://people.cs.aau.dk/~adavid/UDBM/Google Scholar
- D. Georgakopoulos and M.P. Papazoglou (Eds.). 2008. Service-oriented Computing. MIT Press, Cambridge, MA, USA. https://mitpress.mit.edu/books/service-oriented-computing Google ScholarDigital Library
- S. Günther and T. Berger. 2008. Service-Oriented Product Lines: Towards A Development Process and Feature Management Model for Web Services. In Proceedings 2nd Workshop on Service-Oriented Architectures and Software Product Lines: Putting Both Together (SOAPL'08), R.W. Krut and S.G. Cohen (Eds.). Lero Centre, University of Limerick, Ireland, 131--136. http://www.cse.chalmers.se/~bergert/paper/2008-soapl-webservices.pdf.Google Scholar
- A. Halin, A. Nuttinck, M. Acher, X. Devroey, G. Perrouin, and P. Heymans. 2017. Yo Variability! JHipster: A Playground for Web-apps Analyses. In Proceedings 11th International Workshop on Variability Modelling of Software-intensive Systems (VaMoS'17), M.H. ter Beek, N. Siegmund, and I. Schaefer (Eds.). ACM, 44--51. Google ScholarDigital Library
- P. Juodisius, A. Sarkar, R.R. Mukkamala, M. Antkiewicz, K. Czarnecki, and A. Wąsowski. 2016. Clafer: Lightweight Modeling of Structure and Behavior with Variability. (2016). Unpublished manuscript.Google Scholar
- C. Laneve and L. Padovani. 2015. An algebraic theory for web service contracts. Form. Asp. Comp. 27, 4 (2015), 613--640. Google ScholarCross Ref
- A. Legay and L.-M. Traonouez. 2013. PyEcdar: Towards Open Source Implementation for Timed Systems. In Proceedings 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13) (LNCS), D. Van Hung and M. Ogawa (Eds.), Vol. 8172. Springer, 460--463. See also https://project.inria.fr/pyecdar/.Google ScholarCross Ref
- M. Mannion. 2002. Using First-Order Logic for Product Line Model Validation. In Proceedings 2nd International Software Product Lines Conference (SPLC'02) (LNCS), G.J. Chastek (Ed.), Vol. 2379. Springer, 176--187. Google ScholarDigital Library
- F.M. Medeiros, E.S. de Almeida, and S.R. de Lemos Meira. 2009. Towards an Approach for Service-Oriented Product Line Architectures. In Proceedings 3rd Workshop on Service-Oriented Architectures and Software Product Lines: Enhancing Variation (SOAPL'09), R.W. Krut and S.G. Cohen (Eds.). Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, USA, 151--157.Google Scholar
- J. Meinicke, T. Thüm, R Schröter, F. Benduhn, T. Leich, and G. Saake. 2017. Mastering Software Variability with FeatureIDE. Springer, Cham, Switzerland. Google ScholarDigital Library
- OASIS. 2007. Web Services Business Process Execution Language Version 2.0. Retrieved Nov 2, 2017 from http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.htmlGoogle Scholar
- M. Raatikainen, V. Myllärniemi, and T. Männistö. 2007. Comparison of Service and Software Product Family Modeling. In Proceedings 1st Workshop on Service-Oriented Architectures and Software Product Lines: What is the Connection? (SOAPL'07), S. Cohen and R. Krut (Eds.). Special Report CMU/SEI-2008-SR-006, Carnegie Mellon University, Pittsburgh, PA, USA, C:1--C:10. https://resources.sei.cmu.edu/asset_files/SpecialReport/2008_003_001_14906.pdf.Google Scholar
- P.J. Ramadge and W.M. Wonham. 1987. Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25, 1 (1987), 206--230. Google ScholarDigital Library
- Q. Yi, X. Liu, A. Bouguettaya, and B. Medjahed. 2008. Deploying and managing Web services: issues, solutions, and directions. VLDB J. 17, 3 (2008), 735--572. Google ScholarDigital Library
Index Terms
- Modelling and analysis with featured modal contract automata
Recommendations
Orchestration of Dynamic Service Product Lines with Featured Modal Contract Automata
SPLC '17: Proceedings of the 21st International Systems and Software Product Line Conference - Volume BIn Service-Oriented Computing, contracts provide a way to characterise the behavioural conformance of a composition of services, and to guarantee that the results do not lead to spurious compositions. Adding variability leads to a product line of ...
Controller synthesis of service contracts with variability
AbstractService contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level ...
Timed service contract automata
AbstractWe equip a recently developed model for the specification of service contracts with real-time constraints. Service contracts offer a means to define the behavioural compliance of a composition of services, typically dictated in a service-level ...
Comments