Verificación y depuración
URI permanente para esta colección:
Artículos en la categoría Verificación y depuración publicados en las Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo Runtime Verification of Timed Petri Net Product LinesGómez-Martínez, Elena; Requeno, Jose Ignacio. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.Petri Net Product Line (PNPL) is a type of Petri net focusing on the variability of reconfigurable industrial pipelines. This paper defines Timed Petri Net Product Lines (TPNPL), which incorporate time duration to PNPL as first-class citizens. TPNPLs rely on Coloured Petri Nets (CPN) for the notion of time. Additionally, we provide means for analysing TPNPL by runtime verification. The runtime verification features are implemented on top of the TeSSLa framework, which is composed by a TeSSLa language and interpreter. The TeSSLa interpreter receives the simulation of a TPNPL as a set of execution traces, the properties to analyse formalised in the TeSSLa language, and outputs an evaluation report. We update Titan, a modelling framework for the analysis of PNPL in Eclipse, in order to support the new features. To this end, Titan provides an automatic transformation of TPNPL into CPN, runs the CPN Tools engine for the simulation process, and forwards the execution traces and properties to the TeSSLa framework. Titan transparently coordinates all these steps.Artículo A Domain-Specific Language for Real-Time Critical SystemsParra, Pablo; Ceresa, Martin; Moreno, Elsa; Rodríguez Polo, Óscar; Sánchez, César. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.Software development for real-time critical systems is hard, complex and challenging. In real-time critical systems, the imposed requirements are not solely functional, but they also establish a set of temporal constraints that the system must meet to ensure its correct operation. Moreover, validation and verification costs of software development projects for hard real-time critical systems, such as on-board satellite systems, in most cases account for more than half of the total project cost. In this work-in-progress, we introduce a new domain-specific language targetting real-time critical systems aimed at reducing validation and verification costs. The language includes real-time reactive systems abstractions as language citizens, making programs clearer and easier to reason about than current implementations in C or Ada. Moreover, we build the language around two main principles: restricted memory management and every fragment written by users should terminate.Artículo Rule and Constraint based Debugging of DBpedia QueriesAlmendros-Jimenez, Jesus M.; Becerra-Teron, Antonio. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.DBpedia constitutes the main resource for Linked Open Data on the Web and represents the largest Knowledge Graph to date. The SPARQL query language is typically used to query DBpedia resources from the DBpedia SPARQL endpoint. Despite the simplicity of SPARQL, queries can have errors. According to a recent study that analyzes the execution of SPARQL endpoints, 66.9% have runtime errors; and 20.0% have no errors, but return empty results. Adjusting a query to what the user expects is a challenging task. In this paper, we propose a debug- ging method for DBpedia queries whose goal is to accommodate a given query to a set of expected and unexpected answers. Through a transla- tion from SPARQL to rules, the debugger finds a similar query that fits the requirements. The debugger uses constraint solving to look for filter conditions that match the expected and unexpected answers. The paper presents a practical application of rule systems and constraint solving in databases, and, more concretely, in DBpedia, enabling in real time the adjustment of queries to real datasets.