This paper reports a mechanism to incorporate Linear Temporal Logic (LTL) for a component-based software architectural configuration specified by the ρarq -calculus. This process was made through the translation of the system definition, structure and behavior, to Atomic Propositions Transition System (APTS), upon which, the verification of one property was performed using LTL. The PintArq software application was extended to support this mechanism. One example ilustrates the verification of responsiveness, a subtype of liveness property.
CITATION STYLE
Puentes, O. J., & Diosa, H. A. (2018). Linear temporal logic applied to component-based software architectural models specified through ρarq calculus. In Communications in Computer and Information Science (Vol. 915, pp. 393–405). Springer Verlag. https://doi.org/10.1007/978-3-030-00350-0_33
Mendeley helps you to discover research relevant for your work.