{"id":974,"date":"2021-04-25T18:32:23","date_gmt":"2021-04-25T16:32:23","guid":{"rendered":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/"},"modified":"2021-04-25T18:32:23","modified_gmt":"2021-04-25T16:32:23","slug":"phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties","status":"publish","type":"events","link":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/","title":{"rendered":"PhD Defense: Specification and model-driven trace checking of complex temporal properties"},"content":{"rendered":"

To join the PhD defense, click here<\/a>.<\/p>

Abstract<\/strong>:<\/p>

Offline trace checking is a procedure used to evaluate requirement properties over a\u00a0trace of recorded events. System properties verified in the context of trace checking can be\u00a0specified using different specification languages and formalisms; in this thesis, we consider\u00a0two classes of complex temporal properties:<\/p>

  1. properties defined using aggregation operators;<\/li>
  2. signal-based temporal properties from the Cyber Physical System (CPS) domain.\u00a0The overall goal of this dissertation is to develop methods and tools for the specification\u00a0and trace checking of the aforementioned classes of temporal properties, focusing on the\u00a0development of scalable trace checking procedures for such properties.<\/li><\/ol><\/p>

    The main contributions of this thesis are:<\/p>

    • the TEMPSY-CHECK-AG model-driven approach for trace checking of temporal properties\u00a0with aggregation operators, defined in the TemPsy-AG language;<\/li>
    • a taxonomy covering the most common types of Signal-based Temporal Properties (SBTPs)\u00a0in the CPS domain;<\/li>

    • SB-TemPsy, a trace-checking approach for SBTPs that strikes a good balance in industrial\u00a0contexts in terms of efficiency of the trace checking procedure and coverage of the most\u00a0important types of properties in CPS domains.\u00a0SB-TemPsy includes:\u00a0<\/p>

      • SB-TemPsy-DSL,\u00a0a DSL that allows the specification of the types of SBTPs identified in the aforementioned taxonomy, and 2) an efficient trace-checking procedure, implemented in a prototype\u00a0tool called\u00a0SB-TemPsy-Check;<\/li><\/ul><\/li>
      • TD-SB-TemPsy-Report, a model-driven trace diagnostics approach for SBTPs expressed\u00a0in SB-TemPsy-DSL. TD-SB-TemPsy-Report relies on a set of diagnostics patterns, i.e., undesired\u00a0signal behaviors that might lead to property violations. To provide relevant and\u00a0detailed information about the cause of a property violation, TD-SB-TemPsy-Report determines\u00a0the diagnostics information specific to each type of diagnostics pattern.<\/li><\/ul>

        Our technological contributions rely on model-driven approaches for trace checking and\u00a0trace diagnostics. Such approaches consist in reducing the problem of checking (respectively,\u00a0determining the diagnostics information of) a property \u00a0p\u00a0over an execution trace\u00a0\u039b\u00a0to the\u00a0problem of evaluating an OCL (Object Constraint Language) constraint (semantically equivalent\u00a0to p) on an instance (equivalent to\u00a0\u039b) of a meta-model of the trace. The results in\u00a0terms of efficiency of our model-driven tools\u00a0presented in this thesis are in line with those\u00a0presented in previous work, and confirm that model-driven technologies can lead to the development\u00a0of tools that exhibit good performance from a practical standpoint, also when\u00a0applied in industrial contexts.<\/p><\/div><\/section>","protected":false},"excerpt":{"rendered":"

        To join the PhD defense, click here.<\/p>\n","protected":false},"author":0,"featured_media":975,"parent":0,"menu_order":0,"comment_status":"open","ping_status":"closed","template":"","format":"standard","meta":{"featured_image_focal_point":[],"show_featured_caption":false,"ulux_newsletter_groups":"","uluxPostTitle":"","uluxPrePostTitle":"","_trash_the_other_posts":false,"_price":"","_stock":"","_tribe_ticket_header":"","_tribe_default_ticket_provider":"","_tribe_ticket_capacity":"0","_ticket_start_date":"","_ticket_end_date":"","_tribe_ticket_show_description":"","_tribe_ticket_show_not_going":false,"_tribe_ticket_use_global_stock":"","_tribe_ticket_global_stock_level":"","_global_stock_mode":"","_global_stock_cap":"","_tribe_rsvp_for_event":"","_tribe_ticket_going_count":"","_tribe_ticket_not_going_count":"","_tribe_tickets_list":"[]","_tribe_ticket_has_attendee_info_fields":false,"event_start_date":"2021-04-29 15:00:00","event_end_date":"2021-04-29 18:00:00","event_speaker_name":"Chaima Boufaied (SVV research group)","event_speaker_link":"","event_is_online":false,"event_location":"","event_street":"","event_location_link":"","event_zip_code":"","event_city":"","event_country":"LU"},"events-topic":[],"events-type":[],"organisation":[183],"authorship":[],"acf":[],"yoast_head":"\nPhD Defense: Specification and model-driven trace checking of complex temporal properties - SnT - Universit\u00e9 du Luxembourg I Uni.lu<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/\" \/>\n<meta property=\"og:locale\" content=\"fr_FR\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"PhD Defense: Specification and model-driven trace checking of complex temporal properties\" \/>\n<meta property=\"og:description\" content=\"To join the PhD defense, click here.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/\" \/>\n<meta property=\"og:site_name\" content=\"SnT FR\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2026\/03\/03112647\/SNT_SM-Profile_1600x1600px-scaled.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"2560\" \/>\n\t<meta property=\"og:image:height\" content=\"2560\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Dur\u00e9e de lecture estim\u00e9e\" \/>\n\t<meta name=\"twitter:data1\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/\",\"url\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/\",\"name\":\"PhD Defense: Specification and model-driven trace checking of complex temporal properties - SnT - Universit\u00e9 du Luxembourg I Uni.lu\",\"isPartOf\":{\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2021\/04\/phd_defense_specification_and_model_driven_trace_checking_of_complex_temporal_properties.jpg\",\"datePublished\":\"2021-04-25T16:32:23+00:00\",\"dateModified\":\"2021-04-25T16:32:23+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#breadcrumb\"},\"inLanguage\":\"fr-FR\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#primaryimage\",\"url\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2021\/04\/phd_defense_specification_and_model_driven_trace_checking_of_complex_temporal_properties.jpg\",\"contentUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2021\/04\/phd_defense_specification_and_model_driven_trace_checking_of_complex_temporal_properties.jpg\",\"width\":2377,\"height\":2381},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/www.uni.lu\/fr\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Interdisciplinary Centre for Security, Reliability and Trust (SnT)\",\"item\":\"https:\/\/www.uni.lu\/snt-fr\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Events\",\"item\":\"https:\/\/www.uni.lu\/snt-fr\/events\/\"},{\"@type\":\"ListItem\",\"position\":4,\"name\":\"PhD Defense: Specification and model-driven trace checking of complex temporal properties\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/#website\",\"url\":\"https:\/\/www.uni.lu\/snt-fr\/\",\"name\":\"SnT\",\"description\":\"Interdisciplinary Centre for Security, Reliability and Trust I Uni.lu\",\"publisher\":{\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/#organization\"},\"alternateName\":\"Interdisciplinary Centre for Security, Reliability and Trust I Universit\u00e9 du Luxembourg\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.uni.lu\/snt-fr\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"fr-FR\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/#organization\",\"name\":\"SnT - Universit\u00e9 du Luxembourg I Uni.lu\",\"alternateName\":\"Interdisciplinary Centre for Security, Reliability and Trust\",\"url\":\"https:\/\/www.uni.lu\/snt-fr\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"fr-FR\",\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2026\/03\/03112647\/SNT_SM-Profile_1600x1600px-scaled.jpg\",\"contentUrl\":\"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2026\/03\/03112647\/SNT_SM-Profile_1600x1600px-scaled.jpg\",\"width\":2560,\"height\":2560,\"caption\":\"SnT - Universit\u00e9 du Luxembourg I Uni.lu\"},\"image\":{\"@id\":\"https:\/\/www.uni.lu\/snt-fr\/#\/schema\/logo\/image\/\"},\"sameAs\":[\"https:\/\/www.linkedin.com\/school\/snt-lu\/\"]}]}<\/script>\n<!-- \/ Yoast SEO Premium plugin. -->","yoast_head_json":{"title":"PhD Defense: Specification and model-driven trace checking of complex temporal properties - SnT - Universit\u00e9 du Luxembourg I Uni.lu","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/","og_locale":"fr_FR","og_type":"article","og_title":"PhD Defense: Specification and model-driven trace checking of complex temporal properties","og_description":"To join the PhD defense, click here.","og_url":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/","og_site_name":"SnT FR","og_image":[{"width":2560,"height":2560,"url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2026\/03\/03112647\/SNT_SM-Profile_1600x1600px-scaled.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Dur\u00e9e de lecture estim\u00e9e":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/","url":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/","name":"PhD Defense: Specification and model-driven trace checking of complex temporal properties - SnT - Universit\u00e9 du Luxembourg I Uni.lu","isPartOf":{"@id":"https:\/\/www.uni.lu\/snt-fr\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#primaryimage"},"image":{"@id":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#primaryimage"},"thumbnailUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2021\/04\/phd_defense_specification_and_model_driven_trace_checking_of_complex_temporal_properties.jpg","datePublished":"2021-04-25T16:32:23+00:00","dateModified":"2021-04-25T16:32:23+00:00","breadcrumb":{"@id":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#breadcrumb"},"inLanguage":"fr-FR","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/"]}]},{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#primaryimage","url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2021\/04\/phd_defense_specification_and_model_driven_trace_checking_of_complex_temporal_properties.jpg","contentUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2021\/04\/phd_defense_specification_and_model_driven_trace_checking_of_complex_temporal_properties.jpg","width":2377,"height":2381},{"@type":"BreadcrumbList","@id":"https:\/\/www.uni.lu\/snt-fr\/events\/phd-defense-specification-and-model-driven-trace-checking-of-complex-temporal-properties\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.uni.lu\/fr"},{"@type":"ListItem","position":2,"name":"Interdisciplinary Centre for Security, Reliability and Trust (SnT)","item":"https:\/\/www.uni.lu\/snt-fr\/"},{"@type":"ListItem","position":3,"name":"Events","item":"https:\/\/www.uni.lu\/snt-fr\/events\/"},{"@type":"ListItem","position":4,"name":"PhD Defense: Specification and model-driven trace checking of complex temporal properties"}]},{"@type":"WebSite","@id":"https:\/\/www.uni.lu\/snt-fr\/#website","url":"https:\/\/www.uni.lu\/snt-fr\/","name":"SnT","description":"Interdisciplinary Centre for Security, Reliability and Trust I Uni.lu","publisher":{"@id":"https:\/\/www.uni.lu\/snt-fr\/#organization"},"alternateName":"Interdisciplinary Centre for Security, Reliability and Trust I Universit\u00e9 du Luxembourg","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.uni.lu\/snt-fr\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"fr-FR"},{"@type":"Organization","@id":"https:\/\/www.uni.lu\/snt-fr\/#organization","name":"SnT - Universit\u00e9 du Luxembourg I Uni.lu","alternateName":"Interdisciplinary Centre for Security, Reliability and Trust","url":"https:\/\/www.uni.lu\/snt-fr\/","logo":{"@type":"ImageObject","inLanguage":"fr-FR","@id":"https:\/\/www.uni.lu\/snt-fr\/#\/schema\/logo\/image\/","url":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2026\/03\/03112647\/SNT_SM-Profile_1600x1600px-scaled.jpg","contentUrl":"https:\/\/www.uni.lu\/wp-content\/uploads\/sites\/13\/2026\/03\/03112647\/SNT_SM-Profile_1600x1600px-scaled.jpg","width":2560,"height":2560,"caption":"SnT - Universit\u00e9 du Luxembourg I Uni.lu"},"image":{"@id":"https:\/\/www.uni.lu\/snt-fr\/#\/schema\/logo\/image\/"},"sameAs":["https:\/\/www.linkedin.com\/school\/snt-lu\/"]}]}},"_links":{"self":[{"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/events\/974"}],"collection":[{"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/events"}],"about":[{"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/types\/events"}],"replies":[{"embeddable":true,"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/comments?post=974"}],"version-history":[{"count":0,"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/events\/974\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/media\/975"}],"wp:attachment":[{"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/media?parent=974"}],"wp:term":[{"taxonomy":"events-topic","embeddable":true,"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/events-topic?post=974"},{"taxonomy":"events-type","embeddable":true,"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/events-type?post=974"},{"taxonomy":"organisation","embeddable":true,"href":"https:\/\/www.uni.lu\/snt-fr\/wp-json\/wp\/v2\/organisation?post=974"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}