In a perspective of an incremental and iterative formal development of software, models should preserve a refinement relation with already existing specifications models. In cases where a model is not a refinement of a specification model, it should be modified in order to create a refinement relation between them. This paper proposes a refinement repair algorithm guided through an analysis of the refinement game between a specification model and another model that is not related by a refinement relation. We are interested in models expressed as Kripke Modal Transitions Systems (KMTS) which are appropriate to represent partial information of systems.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Bulychev, P., Konnov, I., Zakharov, V.: Computing (bi) simulation relations preserving ctl* x. for ordinary and fair kripke structures. Math. Methods Algorithms Inst. Syst. Program. Russ. Acad. Sci.
12 (2007)
5.
Chatzieleftheriou, G., Bonakdarpour, B., Smolka, S.A., Katsaros, P.: Abstract model repair. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 341–355. Springer, Heidelberg (2012). doi:
10.1007/978-3-642-28891-3_32CrossRef
6.
Guerra, P.T., Andrade, A., Wassermann, R.: Toward the revision of CTL models through kripke modal transition systems. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 115–130. Springer, Heidelberg (2013). doi:
10.1007/978-3-642-41071-0_9CrossRef
7.
Sabetzadeh, M., Easterbrook, S.: Analysis of inconsistency in graph-based viewpoints: a category-theoretical approach. In: 18th IEEE International Conference on Automated Software Engineering, pp. 12–21. IEEE (2003)
8.
Stirling, C.: Local model checking games (extended abstract). In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995). doi:
10.1007/3-540-60218-6_1CrossRef
9.
Thomas, W.: On the Ehrenfeucht-Fraïssé game in theoretical computer science. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 559–568. Springer, Heidelberg (1993). doi:
10.1007/3-540-56610-4_89CrossRef
10.
Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng.
29(2), 99–115 (2003)
CrossRef
11.
Wang, F., Cheng, C.-H.: Program repair suggestions from graphical state-transition specifications. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 185–200. Springer, Heidelberg (2008). doi:
10.1007/978-3-540-68855-6_12CrossRef
Über dieses Kapitel
Titel
A Refinement Repair Algorithm Based on Refinement Game for KMTS Models
Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.
Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis. Jetzt gratis downloaden!
