A Symbolic Execution-Based Approach to Model Transformation Verification Using Structural Contracts
Bibliographic record
Abstract
As the complexity of software systems increases, the engineering effort for developing those systems must deal with that complexity.One paradigm for software development is model-driven engineering, where the models of the system become the first-order artefacts.These models may be used for simulation or analysis of the system, or be transformed into executable code or documentation.The intention is to represent each facet in the system in the most appropriate formalism at the most appropriate level of abstraction.Model transformations provide a structured and understandable way of manipulating these models, and are often rooted in a mathematical approach which enables precise specification and analysis.However, it may be difficult for a user to reason about what elements will be matched and written by a particular transformation.Our research is focused on the verification of model transformations for a particular model transformation language.In particular, we are interested in the proving of pre-condition/ post-condition contracts, which relate the elements in the input models to the transformation with the elements present in the corresponding output elements.i DSLTrans Ce langage de transformation DSLTrans a été sélectionné pour la vérification en raison des propriétés garanties par construction : terminaison et confluence.Dans cette thèse, nous fournissons une description de la sémantique de DSLTrans dans l'approche « double-pushout », qui apporte DSLTrans au point dans les transformations des modèles.De plus, nous fournissons les sémantiques pour d'autres constructions DSLTrans qui ne sont pas considérées dans des travaux antérieurs.Ces constructions comprennent des éléments négatifs, liens indirects, et éléments «Existe».Preuve de Contrat L'idée de base de notre approche de vérification des contrats est de construire des conditions de trajet pour la transformation DSLTrans à travers une procédure d'exécution symbolique.Autrement dit, notre technique détermine toutes les combinaisons valides de règles dans la transformation.Chacune de ces conditions de trajet représentera explicitement les éléments intrant et extrants présents lorsque cette combinaison des règles de transformation s'exécute à travers une relation d'abstraction.Nous vérifions ensuite les contrats de précondition / post-condition sur ces conditions de trajet.Si une condition de trajet ne satisfait pas le contrat, la condition de trajet sert de contrexemple.L'examen de ce contrexemple permet de raisonner sur les règles et l'interaction des règles dans la transformation.En tant que contribution de cette thèse, nous considérons toutes les constructions dans le langage DSLTrans et ainsi nous pouvons vérifier toutes les transformations DSLTrans, y compris celles qui contiennent des éléments négatifs.De plus, dans cette thèse, nous définissons également l'unique morphisme de division, ce qui permet aux sommets dans le graphique de modèle de se «diviser» sur les sommets dans le graphique cible.L'utilisation de ce morphisme nous permet de créer moins de conditions de trajets que dans les recherches précédentes, permettant à notre technique d'évoluer vers de plus grandes transformations.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.002 | 0.007 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.002 |
| Scholarly communication | 0.002 | 0.003 |
| Open science | 0.002 | 0.003 |
| Research integrity | 0.001 | 0.002 |
| Insufficient payload (model declined to judge) | 0.011 | 0.002 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".