References of "Gonzalez Perez, Carlos Alberto 50024799"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailSmart Bound Selection for the Verification of UML/OCL Class Diagrams
Clarisó, Robert; Gonzalez Perez, Carlos Alberto UL; Cabot, Jordi

in IEEE Transactions on Software Engineering (in press)

Correctness of UML class diagrams annotated with OCL constraints can be checked using bounded verification techniques, e.g., SAT or constraint programming (CP) solvers. Bounded verification detects faults ... [more ▼]

Correctness of UML class diagrams annotated with OCL constraints can be checked using bounded verification techniques, e.g., SAT or constraint programming (CP) solvers. Bounded verification detects faults efficiently but, on the other hand, the absence of faults does not guarantee a correct behavior outside the bounded domain. Hence, choosing suitable bounds is a non-trivial process as there is a trade-off between the verification time (faster for smaller domains) and the confidence in the result (better for larger domains). Unfortunately, bounded verification tools provide little support in the bound selection process. In this paper, we present a technique that can be used to (i) automatically infer verification bounds whenever possible, (ii) tighten a set of bounds proposed by the user and (iii) guide the user in the bound selection process. This approach may increase the usability of UML/OCL bounded verification tools and improve the efficiency of the verification process. [less ▲]

Detailed reference viewed: 64 (18 UL)
Full Text
Peer Reviewed
See detailEnabling Model Testing of Cyber-Physical Systems
Gonzalez Perez, Carlos Alberto UL; Varmazyar, Mojtaba UL; Nejati, Shiva UL et al

in Proceedings of ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems (MODELS’18) (2018, October)

Applying traditional testing techniques to Cyber-Physical Systems (CPS) is challenging due to the deep intertwining of software and hardware, and the complex, continuous interactions between the system ... [more ▼]

Applying traditional testing techniques to Cyber-Physical Systems (CPS) is challenging due to the deep intertwining of software and hardware, and the complex, continuous interactions between the system and its environment. To alleviate these challenges we propose to conduct testing at early stages and over executable models of the system and its environment. Model testing of CPSs is however not without difficulties. The complexity and heterogeneity of CPSs renders necessary the combination of different modeling formalisms to build faithful models of their different components. The execution of CPS models thus requires an execution framework supporting the co-simulation of different types of models, including models of the software (e.g., SysML), hardware (e.g., SysML or Simulink), and physical environment (e.g., Simulink). Furthermore, to enable testing in realistic conditions, the co-simulation process must be (1) fast, so that thousands of simulations can be conducted in practical time, (2) controllable, to precisely emulate the expected runtime behavior of the system and, (3) observable, by producing simulation data enabling the detection of failures. To tackle these challenges, we propose a SysML-based modeling methodology for model testing of CPSs, and an efficient SysML-Simulink co-simulation framework. Our approach was validated on a case study from the satellite domain. [less ▲]

Detailed reference viewed: 23 (2 UL)