Using Symbolic Dates of the Linear Logic to Verify Performance Requirements in SOA Models

  • Kênia Santos de Oliveira
  • Stéphane Julia
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 800)


This article presents an approach for performance verification of requirement scenarios in Service-Oriented Architecture (SOA) models. The SOA models are represented by Interorganizational WorkFlow nets that are not necessarily deadlock-free. The requirement model considered in this article defines functionalities that are of interest of all parties involved in the process, for this reason is considered as a public model. An architectural model is considered as a private model since it is composed of a set of private processes that interact through asynchronous communication mechanisms. For the scenarios of the architectural and requirement models that are equivalent in terms of behaviour (or bisimulation) symbolic dates associated with the activities of the processes can be produced from the calculation of the Linear Logic sequents. Symbolic dates can be used to verify if an architectural model scenario that simulates the behavior of a requirement model scenario is also equivalent in terms of performance. To illustrate the proposed approach an example was considered and from this example it was possible to observe that the approach can be useful to indicate if a architectural model in the context of SOA satisfy the performance of business needs defined by a requirement model.


Interorganizational WorkFlow net Time Petri nets Linear Logic Service-Oriented Architecture Non-functional requirement verification 


  1. 1.
    Hoyos, H., Casallas, R., Jiménez, F.: Hiles-t: an ADL for early requirement verification of embedded systems. In: Proceedings of the 5th International Workshop on Model Based Architecting and Construction of Embedded Systems, pp. 7–12. ACM (2012)Google Scholar
  2. 2.
    Goknil, A., Kurtev, I., Berg, K.V.D.: Generation and validation of traces between requirements and architecture based on formal trace semantics. J. Syst. Softw. 88, 112–137 (2014)CrossRefGoogle Scholar
  3. 3.
    O’Brien, L., Merson, P., Bass, L.: Quality attributes for service-oriented architectures. In: Proceedings of the International Workshop on Systems Development in SOA Environments, SDSOA ’07, Washington, DC, p. 3. IEEE Computer Society (2007)Google Scholar
  4. 4.
    Grundy, J., Hosking, J., Li, L., Liu, N.: Performance engineering of service compositions. In: Proceedings of the 2006 International Workshop on Service-oriented Software Engineering, SOSE ’06, pp. 26–32. ACM, New York (2006)Google Scholar
  5. 5.
    Oliveira, K.S., de Oliveira, V.F., Julia, S.: Using linear logic to verify requirement scenarios in SOA models based on interorganizational workflow nets relaxed sound. In: 19th International Conference on Enterprise Information Systems (2017)Google Scholar
  6. 6.
    van der Aalst, W.M.P.: Loosely coupled interorganizational workflows: modeling and analyzing workflows crossing organizational boundaries. Inf. Manag. 37, 67–75 (2000)CrossRefGoogle Scholar
  7. 7.
    van der Aalst, W.M.P.: Modeling and analyzing interorganizational workflows. In: International Conference on Application of Concurrency to System Design, pp. 262–272. IEEE Computer Society Press, 1998Google Scholar
  8. 8.
    Fahland, D., Favre, C., Koehler, J., Lohmann, N., Volzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70, 448–466 (2011)CrossRefGoogle Scholar
  9. 9.
    Passos, L.M.S.: A metodology based on linear logic for interorganizational workflow processes analysis. Ph.D. dissertation, Federal University of Uberlândia (2016)Google Scholar
  10. 10.
    Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. dissertation (1974) aAI7511026Google Scholar
  11. 11.
    Ramchandani, C.: Analysis of asynchronous concurrent systems by timed petri nets. Ph.D. dissertation, Massachusetts Institute of Technology, Cambridge (1973)Google Scholar
  12. 12.
    Ling, S., Schmidt, H.: Time petri nets for workflow modelling and analysis. In: 2000 IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 3039–3044. IEEE (2000)Google Scholar
  13. 13.
    Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Girault, F., Pradin-Chezalviel, B., Valette, R.: A logic for petri nets. Journal Européen des Systèmes Automatisés 31, 525–542 (1997)zbMATHGoogle Scholar
  15. 15.
    Riviere, N., Pradin-Chezalviel, B., Valette, R.: Reachability and temporal conflicts in t-time petri nets. In: 9th International Workshop on Petri Nets and Performance Models (2001)Google Scholar
  16. 16.
    Valette, R.: Analysis of petri nets by stepwise refinements. J. Comput. Syst. Sci. 18, 35–46 (1979)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Kênia Santos de Oliveira
    • 1
    • 2
  • Stéphane Julia
    • 3
  1. 1.Computing FacultyFederal University of UberlândiaUberlândiaBrazil
  2. 2.Federal Institute of BrasíliaBrasíliaBrazil
  3. 3.Computing FacultyFederal University of UberlândiaUberlândiaBrazil

Personalised recommendations