Elena Gómez-Martínez – Grupo de I+D en Computación Distribuida (DisCo)

Publicaciones:

2018

E. Gómez-Martínez, R. J. Rodríguez, C. B. Earle, L. E. Elorza, and M. I. Rezaba, “A Methodology for Model-based Verification of Safety Contracts and Performance Requirements,” Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, vol. 232, iss. 3, pp. 227-247, 2018.
[Bibtex]

@Article{GREIB-JRR-18,
author = {Elena G\'{o}mez-Mart\'{i}nez and Ricardo J. Rodr\'{i}guez and Clara Benac Earle and Leire Etxeberria Elorza and Miren Illarramendi Rezaba},
journal = {Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability},
title = {{A Methodology for Model-based Verification of Safety Contracts and Performance Requirements}},
year = {2018},
note = {To appear.},
number = {3},
pages = {227--247},
volume = {232},
abstract = {The verification of safety requirements becomes crucial in critical systems where human lives depend on their correct functioning. Formal methods have often been advocated as necessary to ensure the reliability of software systems, albeit with a considerable effort. In any case, such an effort is cost-effective when verifying safety-critical systems. Often, safety requirements are expressed using safety contracts, in terms of assumptions and guarantees. To facilitate the adoption of formal methods in the safety-critical software industry, we propose a methodology based on well-known modelling languages such as UML and OCL. UML is used to model the software system while OCL is used to express the system safety contracts within UML. In the proposed methodology a UML model enriched with OCL constraints is transformed to a Petri net model that enables to formally verify such safety contracts. The methodology is evaluated on an industrial case study. The proposed approach allows an early safety verification to be performed, which increases the confidence of software engineers while designing the system.},
doi = {10.1177/1748006X16667328},
owner = {ricardo},
timestamp = {2015.10.16},
url = {http://webdiis.unizar.es/~ricardo/files/papers/GREIB-JRR-18.pdf},
}

2015

E. Gómez-Martínez, M. L. Trigueros, F. Sánchez-Figueroa, A. Iglesias-Pérez, J. C. Preciado, R. González-Cabero, and J. Merseguer, “A semantic approach for designing Assistive Software Recommender systems,” Journal of Systems and Software, vol. 104, pp. 166-178, 2015.
[Bibtex]

@Article{Gomez-Martinez2015a,
Title = {A semantic approach for designing Assistive Software Recommender systems},
Author = {Elena G{\'{o}}mez-Mart{\'{\i}}nez and Marino Linaje Trigueros and Fernando S{\'{a}}nchez-Figueroa and Andr{\'{e}}s Iglesias-P{\'{e}}rez and Juan Carlos Preciado and Rafael Gonz{\'{a}}lez-Cabero and Jos{\'{e}} Merseguer},
Journal = {Journal of Systems and Software},
Year = {2015},
Pages = {166--178},
Volume = {104},
Doi = {10.1016/j.jss.2015.03.009},
Url = {http://dx.doi.org/10.1016/j.jss.2015.03.009}
}

E. Gómez-Martínez, R. J. Rodríguez, L. Etxeberria, M. Illarramendi, and C. Benac, “Model-Based Verification of Safety Contracts,” in Proceedings of the 1st International Workshop on Safety and Formal Methods (SaFoMe), 2015, pp. 101-115.
[Bibtex]

@InProceedings{Gomez-Martinez2015,
Title = {{Model-Based Verification of Safety Contracts}},
Author = {Elena G\'{o}mez-Mart\'{i}nez and Ricardo J. Rodr\'{i}guez and Leire Etxeberria and Miren Illarramendi and Clara Benac},
Booktitle = {Proceedings of the 1st International Workshop on Safety and Formal Methods (SaFoMe)},
Year = {2015},
Pages = {101--115},
Publisher = {Springer International Publishing},
Series = {Lecture Notes in Computer Science},
Volume = {8938},
Abstract = {The verification of safety becomes crucial in critical systems where human lives depend on the correct functioning of such systems. Formal methods have often been advocated as necessary to ensure the reliability of software systems, albeit with a considerable effort. In any case, such an effort is cost-effective when verifying safety-critical systems. Safety requirements are usually expressed using safety contracts, in terms of assumptions and guarantees. To facilitate the adoption of formal methods in the safety-critical software industry, we propose the use of well-known modelling languages, such as UML, to model a software system, and the use of OCL to express the system safety contracts within UML. A UML model enriched with OCL constraints is then transformed to a Petri net model that enables to formally verify such safety contracts. We apply our approach to an industrial case study that models a train doors controller in charge of the opening and closing of train doors. Our approach allows to perform an early safety verification, which increases the confidence of software engineers while designing the system.},
Doi = {10.1007/978-3-319-15201-1_7},
ISBN = {978-3-319-15200-4},
Url = {http://webdiis.unizar.es/~ricardo/files/papers/GREIB-SAFOME-15.pdf}
}

2014

E. Gómez-Martínez, R. González-Cabero, and J. Merseguer, “Performance assessment of an architecture with adaptative interfaces for people with special needs,” Empirical Software Engineering, vol. 19, iss. 6, pp. 1967-2018, 2014.
[Bibtex]

@Article{Gomez-Martinez2014,
Title = {Performance assessment of an architecture with adaptative interfaces for people with special needs},
Author = {Elena G{\'{o}}mez-Mart{\'{\i}}nez and Rafael Gonz{\'{a}}lez-Cabero and Jos{\'{e}} Merseguer},
Journal = {Empirical Software Engineering},
Year = {2014},
Number = {6},
Pages = {1967--2018},
Volume = {19},
Doi = {10.1007/s10664-013-9297-1},
Url = {http://dx.doi.org/10.1007/s10664-013-9297-1}
}

R. J. Rodríguez and E. Gómez-Martínez, “Model-based Safety Assessment using OCL and Petri Nets,” in Proceedings of the 40th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), 2014, pp. 56-59.
[Bibtex]

@InProceedings{Rodriguez2014b,
Title = {{Model-based Safety Assessment using OCL and Petri Nets}},
Author = {Rodr\'{i}guez, Ricardo J. and G\'{o}mez-Mart\'{i}nez, Elena},
Booktitle = {Proceedings of the 40th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA)},
Year = {2014},
Month = {Aug},
Pages = {56 -- 59},
Abstract = {Safety becomes a primordial assessment in safety-related systems where human lives can be somehow put in risk, needing to comply with safety requirements defined by industry standards such as IEC 61508, ISO 26262 or DO-178C. Safety contracts are useful to specify these requirements (as assumptions and guarantees), thus assuring an expected level of confidence. To verify the safety requirements is measured to represent more than a half of the overall system development costs. In this paper, we propose a model-based verification that addresses safety verification from the early beginning of system development, thus saving costs. Namely, we use UML for system design and Object Constraint Language (OCL) for specifying safety contracts, while its verification is carried out using Petri nets. As case study, we assess the safety of an embedded system that models a fire prevention system in a hospital building.},
Doi = {10.1109/SEAA.2014.36},
Keywords = {Computational modeling;Contracts;Petri nets;Safety;Software;Unified modeling language;OCL;Petri nets;UML;model-based;safety assessment},
Url = {http://webdiis.unizar.es/~ricardo/files/papers/RG-SEAA-14.pdf}
}

2010

E. Gómez-Martínez and J. Merseguer, “Performance Modeling and Analysis of the Universal Control Hub,” in Computer Performance Engineering – 7th European Performance Engineering Workshop, EPEW 2010, Bertinoro, Italy, September 23-24, 2010. Proceedings, 2010, pp. 160-174.
[Bibtex]

@InProceedings{Gomez-Martinez2010,
Title = {Performance Modeling and Analysis of the Universal Control Hub},
Author = {Elena G{\'{o}}mez-Mart{\'{\i}}nez and Jos{\'{e}} Merseguer},
Booktitle = {Computer Performance Engineering - 7th European Performance Engineering Workshop, {EPEW} 2010, Bertinoro, Italy, September 23-24, 2010. Proceedings},
Year = {2010},
Pages = {160--174},
Doi = {10.1007/978-3-642-15784-4_11},
Url = {http://dx.doi.org/10.1007/978-3-642-15784-4_11}
}