@prefix dcat: <http://www.w3.org/ns/dcat#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix foaf: <http://xmlns.com/foaf/0.1/> .
@prefix vcard: <http://www.w3.org/2006/vcard/ns#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00675778v2> a dcat:Dataset ;
    dct:description """
              Time properties are key requirements for the reliability of Safety Critical Real-Time Systems (RTS). UML and MARTE are standardized modelling languages widely accepted by industrial designers for the design of RTS using Model-Driven Engineering (MDE). However, formal verification at early phases of the system lifecycle for UML-MARTE models remains mainly an open issue. In this paper, we present a time properties verification framework for UML-MARTE safety critical RTS. This framework relies on a property-driven transformation from UML architecture and behaviour models to executable and verifiable models expressed with Time Petri Nets (TPN). Meanwhile, it translates the time properties into a set of property patterns, corresponding to TPN observers. The observer-based model checking approach is then performed on the produced TPN. This verification framework can assess time properties like upper bound for loops and buffers, Best/Worst-Case Response Time, Best/Worst-Case Execution Time, Best/Worst-Case Traversal Time, schedulability, and synchronization-related properties (synchronization, coincidence, exclusion, precedence, sub-occurrence, causality). In addition, it can verify some behavioural properties like absence of deadlock or dead branches. This framework is illustrated with a representative case study. This paper also provides experimental results and evaluates the method's performance.
            """ ;
    dct:identifier "hal-00675778" ;
    dct:issued "2026-05-21T01:46:16.312727"^^xsd:dateTime ;
    dct:language "en" ;
    dct:modified "2026-05-21T01:46:16.312732"^^xsd:dateTime ;
    dct:publisher <https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> ;
    dct:title "Time Properties Verification Framework for UML-MARTE Safety Critical Real-Time Systems" ;
    dcat:contactPoint [ a vcard:Organization ;
            vcard:fn "CCSD" ] ;
    dcat:distribution <https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00675778v2/resource/82daf6d1-5216-4670-b532-8401a3a1a835> ;
    dcat:keyword "infoeu-reposemanticspreprint",
        "infoinfo-escomputer-science-csembedded-systems",
        "infoinfo-secomputer-science-cssoftware-engineering-csse",
        "marte",
        "model-checking",
        "model-transformation",
        "preprints-working-papers-",
        "real-time-system",
        "time-petri-net",
        "time-property-verification",
        "uml" ;
    dcat:landingPage <https://hal.science/hal-00675778> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00675778v2/resource/82daf6d1-5216-4670-b532-8401a3a1a835> a dcat:Distribution ;
    dct:format "HTML" ;
    dct:issued "2026-05-21T01:46:16.323345"^^xsd:dateTime ;
    dct:modified "2026-05-21T01:46:16.267461"^^xsd:dateTime ;
    dct:title "Time Properties Verification Framework for UML-MARTE Safety Critical Real-Time Systems" ;
    dcat:accessURL <https://hal.science/hal-00675778> .

<https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> a foaf:Agent ;
    foaf:name "test_moissonnage_selune" .

<https://hal.science/hal-00675778> a foaf:Document .