Formulating Requirements with FRET for PLCVerif

<!DOCTYPE html> <html lang="en" dir="ltr"> <head> <meta charset="utf-8"> <meta http-equiv="X-UA-Compatible" content="IE=edge"> <meta name="viewport" content="width=device-width, initial-scale=1"> <meta name="generator" content="InvenioRDM 13.0"/> <meta name="description" content="This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements." /> <meta name="citation_title" content="Formulating Requirements with FRET for PLCVerif" /> <meta name="citation_author" content="Adam, Zsofia" /> <meta name="citation_keywords" content="Engineering" /> <meta name="citation_keywords" content="Computing and Computers" /> <meta name="citation_keywords" content="PLCVerif" /> <meta name="citation_keywords" content="PLC" /> <meta name="citation_keywords" content="Programmable Logic Controller" /> <meta name="citation_keywords" content="FRET" /> <meta name="citation_keywords" content="Requirement" /> <meta name="citation_keywords" content="Formal Methods" /> <meta name="citation_keywords" content="Formal Verification" /> <meta name="citation_abstract_html_url" content="https://repository.cern/records/rq11e-47p08" /> <meta property="og:title" content="Formulating Requirements with FRET for PLCVerif" /> <meta property="og:description" content="This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements." /> <meta property="og:url" content="https://repository.cern/records/rq11e-47p08" /> <meta property="og:site_name" content="CDS" /> <meta name="twitter:card" content="summary" /> <meta name="twitter:site" content="" /> <meta name="twitter:title" content="Formulating Requirements with FRET for PLCVerif" /> <meta name="twitter:description" content="This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements." /> <meta name="citation_pdf_url" content="https://repository.cern/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf"/> <link rel="alternate" type="application/pdf" href="https://repository.cern/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf"> <link rel="canonical" href="https://repository.cern/records/rq11e-47p08"> <title>Formulating Requirements with FRET for PLCVerif</title> <link rel="shortcut icon" type="image/x-icon" href="/static/favicon.ico"/> <link rel="apple-touch-icon" sizes="120x120" href="/static/apple-touch-icon-120.png"/> <link rel="apple-touch-icon" sizes="152x152" href="/static/apple-touch-icon-152.png"/> <link rel="apple-touch-icon" sizes="167x167" href="/static/apple-touch-icon-167.png"/> <link rel="apple-touch-icon" sizes="180x180" href="/static/apple-touch-icon-180.png"/> <link rel="stylesheet" href="/static/dist/css/3526.9060f928b1bbb55122ad.css" />   </head> <body data-invenio-config='{"isMathJaxEnabled": "//cdnjs.cloudflare.com/ajax/libs/mathjax/3.2.2/es5/tex-mml-chtml.js?config=TeX-AMS-MML_HTMLorMML"}' itemscope itemtype="http://schema.org/WebPage" data-spy="scroll" data-target=".scrollspy-target"> <a id="skip-to-main" class="ui button primary ml-5 mt-5 skip-link" href="#main">Skip to main</a>  <div> <header class="theme header"> <div class="outer-navbar"> <div class="ui container fluid invenio-header-container mr-0-mobile ml-0-mobile"> <div class="ui container fluid menu-background mr-0-mobile ml-0-mobile"> <div class="ui container mr-0-mobile ml-0-mobile"> <nav id="invenio-nav" class="ui menu inverted p-0"> <div class="borderless item"> <a class="logo-link" href="/"> <img class="ui image rdm-logo" src="/static/images/invenio-rdm.svg" alt="CDS home"/> </a> </div> <div id="rdm-burger-toggle"> <button id="rdm-burger-menu-icon" class="ui button transparent" aria-label="Menu" aria-haspopup="menu" aria-expanded="false" aria-controls="invenio-menu" > <span class="navicon"></span> </button> </div> <div role="menu" id="invenio-menu" aria-labelledby="rdm-burger-menu-icon" class="ui fluid menu borderless mobile-hidden" > <button id="rdm-close-burger-menu-icon" class="ui button transparent" aria-label="Close menu" > <span class="navicon"></span> </button> <div class="item p-0 search-bar"> <div id="header-search-bar" data-options='[{"key": "communities", "text": "In this community", "value": "/communities/summer-student-programme/records"}, {"key": "records", "text": "All CDS", "value": "/search"}]'> <div class="ui fluid search"> <div class="ui icon input"> <input autocomplete="off" aria-label="Search records" placeholder="Search records..." type="text" tabindex="0" class="prompt" value="" > <i aria-hidden="true" class="search icon"></i> </div> </div> </div> </div> <div class="item"> <a role="menuitem" href="/communities">Communities</a> </div> <div class="item"> <a role="menuitem" href="/me/uploads">My dashboard</a> </div> <div class="right menu item"> <form> <a href="/login/?next=%2Frecords%2Frq11e-47p08" class="ui button auth-button" aria-busy="false" aria-live="polite" aria-label="Log in" > <i class="sign-in icon auth-icon" aria-hidden="true"></i> Log in </a> </form> </div> </div> </nav> </div> </div> </div> <div class="ui warning message top attached m-0 inv-banner" id="banner-2"> <div class="ui container"> <p>Due to an <a href="https://cern.service-now.com/service-portal?id=outage&n=OTG0154785">intervention</a> to the underlying infrastructure, the website will not be accessible on Thursday, 6 March 2025, between 12:15 and 12:30 GMT+1. We are sorry for the inconvenience.</p> </div> </div> </header> </div> <main id="main"> <div class="invenio-page-body"> <section id="banners" class="banners" aria-label="Information banner">  <div class="ui fluid container page-subheader-outer with-submenu compact ml-0-mobile mr-0-mobile"> <div class="ui container page-subheader"> <div class="page-subheader-element"> <img class="ui rounded image community-header-logo" src="/static/images/square-placeholder.png" alt="" /> </div> <div class="page-subheader-element"> <div class="ui header"> <a href="/communities/summer-student-programme/records" class="ui small header"> Summer Student Programme </a>  </div> </div> </div> </div>    </section> <div class="ui container"> <div class="ui relaxed grid mt-5"> <div class="two column row top-padded"> <article class="sixteen wide tablet eleven wide computer column main-record-content"> <section id="record-info" aria-label="Publication date and version number"> <div class="ui grid middle aligned"> <div class="two column row"> <div class="left floated left aligned column"> <span class="ui" title="Publication date"> Published September 2, 2022 </span> <span class="label text-muted"> | Version v1</span> </div> <div class="right floated right aligned column"> <span role="note" class="ui label horizontal small neutral mb-5" aria-label="Resource type" > Technical note </span> <span role="note" class="ui label horizontal small access-status open mb-5" data-tooltip="The record and files are publicly accessible." data-inverted="" aria-label="Access status" > <i class="icon unlock" aria-hidden="true"></i> <span aria-label="The record and files are publicly accessible."> Open </span> </span> </div> </div> </div> </section> <div class="ui divider hidden"></div><section id="record-title-section" aria-label="Record title and creators"> <h1 id="record-title" class="wrap-overflowing-text">Formulating Requirements with FRET for PLCVerif</h1> <section id="creatibutors" aria-label="Creators and contributors"> <div class="ui grid"> <div class="row ui accordion affiliations"> <div class="sixteen wide mobile twelve wide tablet thirteen wide computer column"> <h3 class="sr-only">Creators</h3> <ul class="creatibutors"> <li class="creatibutor-wrap separated"> <a class="ui creatibutor-link" href="/search?q=metadata.creators.person_or_org.name%3A%22Adam,+Zsofia%22" > <span class="creatibutor-name">Adam, Zsofia</span></a> <i class="user icon"></i> </li> </ul> </div> </div> <div class="row ui accordion affiliations"> <div class="sixteen wide mobile twelve wide tablet thirteen wide computer column"> <h3>Contributors</h3> <div> <h3 class="creatibutors-header ui small header">Supervisor:</h3> <ul class="creatibutors"> <li class="creatibutor-wrap separated"> <a class="ui creatibutor-link" href="/search?q=metadata.contributors.person_or_org.name%3A%22Borja+Fern%C3%A1ndez+Adiego%22" > <span class="creatibutor-name">Borja Fern谩ndez Adiego</span></a> <i class="user icon"></i> </li> </ul> </div> </div> </div> </div> </section> </section> <section id="description" class="rel-mt-2 rich-input-content" aria-label="Record description"> <h2 id="description-heading" class="sr-only">Description</h2> <div style="word-wrap: break-word;"> This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements. </div> </section> <section id="additional-description-1" class="rel-mt-2 rich-input-content" aria-label="Other"> <h2>Other <span class="text-muted language"></span> </h2> Abbreviations: FRET - Formal Requirements Elicitation Tool </section> <section id="record-files" class="rel-mt-2 rel-mb-3" aria-label="Files"><h2 id="files-heading">Files</h2> <div class="ui accordion panel mb-10 open" href="#files-preview-accordion-panel"> <h3 class="active title panel-heading open m-0"> <div role="button" id="files-preview-accordion-trigger" aria-controls="files-preview-accordion-panel" aria-expanded="true" tabindex="0" class="trigger" aria-label="File preview" > <span id="preview-file-title">cern_report_zsofia_adam.pdf</span> <i class="angle right icon" aria-hidden="true"></i> </div> </h3> <div role="region" id="files-preview-accordion-panel" aria-labelledby="files-preview-accordion-trigger" class="active content preview-container pt-0 open" > <div> <iframe title="Preview" class="preview-iframe" id="preview-iframe" name="preview-iframe" src="/records/rq11e-47p08/preview/cern_report_zsofia_adam.pdf?include_deleted=0" > </iframe> </div> </div> </div> <div class="ui accordion panel mb-10 open" href="#files-list-accordion-panel"> <h3 class="active title panel-heading open m-0"> <div role="button" id="files-list-accordion-trigger" aria-controls="files-list-accordion-panel" aria-expanded="true" tabindex="0" class="trigger"> Files <small class="text-muted"> (539.0 kB)</small> <i class="angle right icon" aria-hidden="true"></i> </div> </h3> <div role="region" id="files-list-accordion-panel" aria-labelledby="files-list-accordion-trigger" class="active content pt-0"> <div> <table class="ui striped table files fluid open"> <thead> <tr> <th>Name</th> <th>Size</th> <th class> <a role="button" class="ui compact mini button right floated archive-link" href="https://repository.cern/api/records/rq11e-47p08/files-archive"> <i class="file archive icon button" aria-hidden="true"></i> Download all </a> </th> </tr> </thead> <tbody> <tr> <td class="ten wide"> <div> <a href="/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf?download=1">cern_report_zsofia_adam.pdf</a> </div> <small class="ui text-muted font-tiny">md5:6e3b609bc7cffcf7c20d35a34fe726b5 <div class="ui icon inline-block" data-tooltip="This is the file fingerprint (checksum), which can be used to verify the file integrity."> <i class="question circle checksum icon"></i> </div> </small> </td> <td>539.0 kB</td> <td class="right aligned"> <span> <a role="button" class="ui compact mini button preview-link" href="/records/rq11e-47p08/preview/cern_report_zsofia_adam.pdf?include_deleted=0" target="preview-iframe" data-file-key="cern_report_zsofia_adam.pdf"> <i class="eye icon" aria-hidden="true"></i>Preview </a> <a role="button" class="ui compact mini button" href="/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf?download=1"> <i class="download icon" aria-hidden="true"></i>Download </a> </span> </td> </tr> </tbody> </table> </div> </div> </div> </section> <section id="additional-details" class="rel-mt-2" aria-label="Additional record details"> <h2 id="record-details-heading">Additional details</h2> <div class="ui divider"></div> <div class="ui grid"> <div class="sixteen wide mobile four wide tablet three wide computer column"> <h3 class="ui header">Identifiers</h3> </div> <div class="sixteen wide mobile twelve wide tablet thirteen wide computer column"> <dl class="details-list"> <dt class="ui tiny header">CDS Reference</dt> <dd> CERN-STUDENTS-Note-2022-107 </dd> </dl> </div> </div> <div class="ui divider"></div> <div class="ui fluid accordion padded grid rel-mb-1"> <div class="active title sixteen wide mobile four wide tablet three wide computer column"> <h3 class="ui header"> <div id="custom-fields-accordion-trigger" role="button" tabindex="0" aria-expanded="true" aria-controls="custom-fields-panel" class="trigger" > <i class="caret right icon" aria-hidden="true"></i>Organization </div> </h3> </div> <div id="custom-fields-panel" role="region" aria-labelledby="custom-fields-accordion-trigger" class="active content sixteen wide mobile twelve wide tablet thirteen wide computer column" > <dl class="details-list"> <dt class="ui tiny header"> Department <a href="https://scientific-info.cern/archives/history_CERN/internal_organisation/20s" aria-label="https://scientific-info.cern/archives/history_CERN/internal_organisation/20s"> <i class="icon external" aria-hidden="true"></i> </a> </dt> <dd> BE </dd> </dl> </div> </div> <div class="ui divider"></div> </section> </article> <aside class="sixteen wide tablet five wide computer column sidebar" aria-label="Record details"> <section id="metrics" aria-label="Metrics" class="ui segment rdm-sidebar sidebar-container"> <div class="ui tiny two statistics rel-mt-1"> <div class="ui statistic"> <div class="value">332</div> <div class="label"> <i aria-hidden="true" class="eye icon"></i> Views </div> </div> <div class="ui statistic"> <div class="value">372</div> <div class="label"> <i aria-hidden="true" class="download icon"></i> Downloads </div> </div> </div> <div class="ui accordion rel-mt-1 centered"> <div class="title"> <i class="caret right icon" aria-hidden="true"></i> <span tabindex="0" class="trigger" data-open-text="Show more details" data-close-text="Show less details" > Show more details </span> </div> <div class="content"> <table id="record-statistics" class="ui definition table fluid"> <thead> <tr> <th></th> <th class="right aligned">All versions</th> <th class="right aligned">This version</th> </tr> </thead> <tbody> <tr> <td> Views <i tabindex="0" role="button" style="position:relative" class="popup-trigger question circle small icon" aria-expanded="false" aria-label="More info" data-variation="mini inverted" > </i> <p role="tooltip" class="popup-content ui flowing popup transition hidden"> Total views </p> </td> <td data-label="All versions" class="right aligned"> 332 </td> <td data-label="This version" class="right aligned"> 332 </td> </tr> <tr> <td> Downloads <i tabindex="0" role="button" style="position:relative" class="popup-trigger question circle small icon" aria-expanded="false" aria-label="More info" data-variation="mini inverted" > </i> <p role="tooltip" class="popup-content ui flowing popup transition hidden"> Total downloads </p> </td> <td data-label="All versions" class="right aligned"> 372 </td> <td data-label="This version" class="right aligned"> 372 </td> </tr> <tr> <td> Data volume <i tabindex="0" role="button" style="position:relative" class="popup-trigger question circle small icon" aria-expanded="false" aria-label="More info" data-variation="mini inverted" > </i> <p role="tooltip" class="popup-content ui flowing popup transition hidden"> Total data volume </p> </td> <td data-label="All versions" class="right aligned">237.7 MB</td> <td data-label="This version" class="right aligned">237.7 MB</td> </tr> </tbody> </table> <p class="text-align-center rel-mt-1"> <small> <a href="/help/statistics">More info on how stats are collected....</a> </small> </p> </div> </div> </section> <div class="sidebar-container"> <h2 class="ui medium top attached header mt-0">Versions</h2> <div id="record-versions" class="ui segment rdm-sidebar bottom attached pl-0 pr-0 pt-0"> <div class="versions"> <div id="recordVersions" data-record='{"access": {"embargo": {"active": false, "reason": null}, "files": "public", "record": "public", "status": "open"}, "created": "2022-08-29T02:00:00+00:00", "custom_fields": {"cern:departments": [{"id": "BE", "title": {"en": "BE"}}]}, "deletion_status": {"is_deleted": false, "status": "P"}, "expanded": {"parent": {"access": {"owned_by": {"active": null, "blocked_at": null, "confirmed_at": null, "email": "", "id": "50701", "is_current_user": null, "links": {"avatar": "https://repository.cern/api/users/50701/avatar.svg"}, "profile": {"affiliations": "", "full_name": "Deleted user"}, "username": "Deleted user", "verified_at": null}}, "communities": {"default": {"access": {"review_policy": "members", "visibility": "public"}, "id": "479178e3-5db9-426b-be8c-4a33317098e3", "links": {"logo": "https://repository.cern/api/communities/479178e3-5db9-426b-be8c-4a33317098e3/logo"}, "metadata": {"description": null, "title": "Summer Student Programme", "type": null}, "slug": "summer-student-programme"}}}}, "files": {"count": 1, "enabled": true, "entries": {"cern_report_zsofia_adam.pdf": {"access": {"hidden": false}, "checksum": "md5:6e3b609bc7cffcf7c20d35a34fe726b5", "ext": "pdf", "id": "40bb8dc4-e32e-47f5-85d5-4ecf53b8c470", "key": "cern_report_zsofia_adam.pdf", "links": {"content": "https://repository.cern/api/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf/content", "iiif_api": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/full/0/default.png", "iiif_base": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf", "iiif_canvas": "https://repository.cern/api/iiif/record:rq11e-47p08/canvas/cern_report_zsofia_adam.pdf", "iiif_info": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/info.json", "self": "https://repository.cern/api/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf"}, "metadata": {}, "mimetype": "application/pdf", "size": 538993, "storage_class": "L"}}, "order": [], "total_bytes": 538993}, "id": "rq11e-47p08", "is_draft": false, "is_published": true, "links": {"access": "https://repository.cern/api/records/rq11e-47p08/access", "access_grants": "https://repository.cern/api/records/rq11e-47p08/access/grants", "access_groups": "https://repository.cern/api/records/rq11e-47p08/access/groups", "access_links": "https://repository.cern/api/records/rq11e-47p08/access/links", "access_request": "https://repository.cern/api/records/rq11e-47p08/access/request", "access_users": "https://repository.cern/api/records/rq11e-47p08/access/users", "archive": "https://repository.cern/api/records/rq11e-47p08/files-archive", "archive_media": "https://repository.cern/api/records/rq11e-47p08/media-files-archive", "communities": "https://repository.cern/api/records/rq11e-47p08/communities", "communities-suggestions": "https://repository.cern/api/records/rq11e-47p08/communities-suggestions", "draft": "https://repository.cern/api/records/rq11e-47p08/draft", "files": "https://repository.cern/api/records/rq11e-47p08/files", "latest": "https://repository.cern/api/records/rq11e-47p08/versions/latest", "latest_html": "https://repository.cern/records/rq11e-47p08/latest", "media_files": "https://repository.cern/api/records/rq11e-47p08/media-files", "parent": "https://repository.cern/api/records/w59n1-asa87", "parent_html": "https://repository.cern/records/w59n1-asa87", "requests": "https://repository.cern/api/records/rq11e-47p08/requests", "reserve_doi": "https://repository.cern/api/records/rq11e-47p08/draft/pids/doi", "self": "https://repository.cern/api/records/rq11e-47p08", "self_html": "https://repository.cern/records/rq11e-47p08", "self_iiif_manifest": "https://repository.cern/api/iiif/record:rq11e-47p08/manifest", "self_iiif_sequence": "https://repository.cern/api/iiif/record:rq11e-47p08/sequence/default", "thumbnails": {"10": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^10,/0/default.jpg", "100": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^100,/0/default.jpg", "1200": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^1200,/0/default.jpg", "250": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^250,/0/default.jpg", "50": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^50,/0/default.jpg", "750": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^750,/0/default.jpg"}, "versions": "https://repository.cern/api/records/rq11e-47p08/versions"}, "media_files": {"count": 0, "enabled": false, "entries": {}, "order": [], "total_bytes": 0}, "metadata": {"additional_descriptions": [{"description": "Abbreviations: FRET - Formal Requirements Elicitation Tool", "type": {"id": "other", "title": {"de": "Sonstige", "en": "Other"}}}], "contributors": [{"person_or_org": {"family_name": "Borja Fern\u00e1ndez Adiego", "name": "Borja Fern\u00e1ndez Adiego", "type": "personal"}, "role": {"id": "supervisor", "title": {"de": "SupervisorIn", "en": "Supervisor"}}}], "creators": [{"person_or_org": {"family_name": "Adam", "given_name": "Zsofia", "identifiers": [{"identifier": "2807895", "scheme": "lcds"}], "name": "Adam, Zsofia", "type": "personal"}}], "description": "This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements.", "identifiers": [{"identifier": "CERN-STUDENTS-Note-2022-107", "scheme": "cds_ref"}], "languages": [{"id": "eng", "title": {"en": "English"}}], "publication_date": "2022-09-02", "publisher": "CERN", "resource_type": {"id": "publication-technicalnote", "title": {"de": "Technical Note", "en": "Technical note"}}, "subjects": [{"id": "Engineering", "scheme": "CERN", "subject": "Engineering"}, {"id": "Computing and Computers", "scheme": "CERN", "subject": "Computing and Computers"}, {"subject": "PLCVerif"}, {"subject": "PLC"}, {"subject": "Programmable Logic Controller"}, {"subject": "FRET"}, {"subject": "Requirement"}, {"subject": "Formal Methods"}, {"subject": "Formal Verification"}], "title": "Formulating Requirements with FRET for PLCVerif"}, "parent": {"access": {"owned_by": {"user": "50701"}, "settings": {"accept_conditions_text": null, "allow_guest_requests": false, "allow_user_requests": false, "secret_link_expiration": 0}}, "communities": {"default": "479178e3-5db9-426b-be8c-4a33317098e3", "entries": [{"access": {"member_policy": "open", "members_visibility": "public", "record_submission_policy": "closed", "review_policy": "members", "visibility": "public"}, "children": {"allow": false}, "created": "2024-12-03T14:34:24.553980+00:00", "custom_fields": {}, "deletion_status": {"is_deleted": false, "status": "P"}, "id": "479178e3-5db9-426b-be8c-4a33317098e3", "links": {}, "metadata": {"title": "Summer Student Programme", "website": "https://careers.cern/summer"}, "revision_id": 7, "slug": "summer-student-programme", "updated": "2024-12-16T08:40:06.380981+00:00"}], "ids": ["479178e3-5db9-426b-be8c-4a33317098e3"]}, "id": "w59n1-asa87", "pids": {}}, "pids": {"oai": {"identifier": "oai:oai:invenio-app-rdm.org::rq11e-47p08", "provider": "oai"}}, "revision_id": 9, "stats": {"all_versions": {"data_volume": 237695913.0, "downloads": 441, "unique_downloads": 372, "unique_views": 332, "views": 594}, "this_version": {"data_volume": 237695913.0, "downloads": 441, "unique_downloads": 372, "unique_views": 332, "views": 594}}, "status": "published", "ui": {"access_status": {"description_l10n": "The record and files are publicly accessible.", "embargo_date_l10n": null, "icon": "unlock", "id": "open", "message_class": "", "title_l10n": "Open"}, "additional_descriptions": [{"description": "Abbreviations: FRET - Formal Requirements Elicitation Tool", "type": {"id": "other", "title_l10n": "Other"}}], "contributors": {"affiliations": [], "contributors": [{"person_or_org": {"family_name": "Borja Fern\u00e1ndez Adiego", "name": "Borja Fern\u00e1ndez Adiego", "type": "personal"}, "role": {"id": "supervisor", "title": "Supervisor"}}]}, "created_date_l10n_long": "August 29, 2022", "creators": {"affiliations": [], "creators": [{"person_or_org": {"family_name": "Adam", "given_name": "Zsofia", "identifiers": [{"identifier": "2807895", "scheme": "lcds"}], "name": "Adam, Zsofia", "type": "personal"}}]}, "custom_fields": {"cern:departments": [{"id": "BE", "title_l10n": "BE"}]}, "description_stripped": "This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements.", "is_draft": false, "languages": [{"id": "eng", "title_l10n": "English"}], "publication_date_l10n_long": "September 2, 2022", "publication_date_l10n_medium": "Sep 2, 2022", "resource_type": {"id": "publication-technicalnote", "title_l10n": "Technical note"}, "updated_date_l10n_long": "January 28, 2025", "version": "v1"}, "updated": "2025-01-28T15:41:31.937890+00:00", "versions": {"index": 1, "is_latest": true}}' data-preview='false'> <div class="rel-p-1"></div> <div class="ui fluid placeholder rel-mr-1 rel-ml-1"></div> <div class="header"> <div class="line"></div> <div class="line"></div> <div class="line"></div> </div> </div> </div> </div> </div><div id="sidebar-communities-manage" data-user-communities-memberships='{}' data-record-community-endpoint="https://repository.cern/api/records/rq11e-47p08/communities" data-record-community-search-endpoint="https://repository.cern/api/records/rq11e-47p08/communities-suggestions" data-record-user-community-search-endpoint="" data-can-manage-record='false' data-pending-communities-search-config='{"aggs": [{"aggName": "type", "field": "type", "title": "Type"}, {"aggName": "status", "field": "status", "title": "Status"}], "appId": "InvenioAppRdm.RecordRequests", "defaultSortingOnEmptyQueryString": [{"sortBy": "newest"}], "initialQueryState": {"filters": [], "hiddenParams": [["expand", "1"], ["is_open", "true"], ["type", "community-inclusion"], ["type", "community-submission"]], "layout": "list", "page": 1, "size": 10, "sortBy": "bestmatch"}, "layoutOptions": {"gridView": false, "listView": true}, "paginationOptions": {"defaultValue": 10, "maxTotalResults": 10000, "resultsPerPage": [{"text": "10", "value": 10}, {"text": "20", "value": 20}, {"text": "50", "value": 50}]}, "searchApi": {"axios": {"headers": {"Accept": "application/json"}, "url": "https://repository.cern/api/records/rq11e-47p08/requests", "withCredentials": true}, "invenio": {"requestSerializer": "InvenioRecordsResourcesRequestSerializer"}}, "sortOptions": [{"sortBy": "bestmatch", "text": "Best match"}, {"sortBy": "newest", "text": "Newest"}, {"sortBy": "oldest", "text": "Oldest"}], "sortOrderDisabled": true}' data-record-community-search-config='{"aggs": [{"aggName": "visibility", "field": "visibility", "title": "Visibility"}, {"aggName": "type", "field": "type", "title": "Type"}], "appId": "InvenioAppRdm.RecordCommunitiesSuggestions", "defaultSortingOnEmptyQueryString": [{"sortBy": "newest"}], "initialQueryState": {"filters": [], "hiddenParams": null, "layout": "list", "page": 1, "size": 10, "sortBy": "bestmatch"}, "layoutOptions": {"gridView": false, "listView": true}, "paginationOptions": {"defaultValue": 10, "maxTotalResults": 10000, "resultsPerPage": [{"text": "10", "value": 10}, {"text": "20", "value": 20}]}, "searchApi": {"axios": {"headers": {"Accept": "application/vnd.inveniordm.v1+json"}, "url": "https://repository.cern/api/records/rq11e-47p08/communities-suggestions", "withCredentials": true}, "invenio": {"requestSerializer": "InvenioRecordsResourcesRequestSerializer"}}, "sortOptions": [{"sortBy": "bestmatch", "text": "Best match"}, {"sortBy": "newest", "text": "Newest"}, {"sortBy": "oldest", "text": "Oldest"}], "sortOrderDisabled": true}' data-record-user-community-search-config='{"aggs": [{"aggName": "visibility", "field": "visibility", "title": "Visibility"}, {"aggName": "type", "field": "type", "title": "Type"}], "appId": "InvenioAppRdm.RecordUserCommunitiesSuggestions", "defaultSortingOnEmptyQueryString": [{"sortBy": "newest"}], "initialQueryState": {"filters": [], "hiddenParams": [["membership", "true"]], "layout": "list", "page": 1, "size": 10, "sortBy": "bestmatch"}, "layoutOptions": {"gridView": false, "listView": true}, "paginationOptions": {"defaultValue": 10, "maxTotalResults": 10000, "resultsPerPage": [{"text": "10", "value": 10}, {"text": "20", "value": 20}]}, "searchApi": {"axios": {"headers": {"Accept": "application/vnd.inveniordm.v1+json"}, "url": "https://repository.cern/api/records/rq11e-47p08/communities-suggestions", "withCredentials": true}, "invenio": {"requestSerializer": "InvenioRecordsResourcesRequestSerializer"}}, "sortOptions": [{"sortBy": "bestmatch", "text": "Best match"}, {"sortBy": "newest", "text": "Newest"}, {"sortBy": "oldest", "text": "Oldest"}], "sortOrderDisabled": true}' data-permissions='{"can_edit": false, "can_manage": false, "can_media_read_files": true, "can_moderate": false, "can_new_version": false, "can_read_files": true, "can_review": false, "can_update_draft": false, "can_view": false}' class="sidebar-container" > <h2 class="ui medium top attached header">Communities</h2> <div class="ui segment bottom attached rdm-sidebar"> <div class="ui fluid placeholder"> <div class="image header"> <div class="line"></div> <div class="line"></div> </div> <div class="image header"> <div class="line"></div> <div class="line"></div> </div> <div class="image header"> <div class="line"></div> <div class="line"></div> </div> </div> </div> </div> <div class="sidebar-container"> <h2 class="ui medium top attached header mt-0">Keywords and subjects</h2> <div id="keywords-and-subjects" aria-label="Keywords and subjects" class="ui segment bottom attached rdm-sidebar"> <h3 class="hidden">Keywords</h3> <ul class="ui horizontal list no-bullets subjects"> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22PLCVerif%22" class="subject" title="Search results for PLCVerif" > PLCVerif </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22PLC%22" class="subject" title="Search results for PLC" > PLC </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22Programmable+Logic+Controller%22" class="subject" title="Search results for Programmable Logic Controller" > Programmable Logic Controller </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22FRET%22" class="subject" title="Search results for FRET" > FRET </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22Requirement%22" class="subject" title="Search results for Requirement" > Requirement </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22Formal+Methods%22" class="subject" title="Search results for Formal Methods" > Formal Methods </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.subject%3A%22Formal+Verification%22" class="subject" title="Search results for Formal Verification" > Formal Verification </a> </li> </ul> <h3 class="ui tiny header">CERN</h3> <ul class="ui horizontal list no-bullets subjects"> <li class="item"> <a href="/search?q=metadata.subjects.id%3A%22Engineering%22" class="subject" title="Search results for Engineering" > Engineering </a> </li> <li class="item"> <a href="/search?q=metadata.subjects.id%3A%22Computing+and+Computers%22" class="subject" title="Search results for Computing and Computers" > Computing and Computers </a> </li> </ul> </div> </div> <div class="sidebar-container"> <h2 class="ui medium top attached header mt-0">Details</h2> <div id="record-details" class="ui segment bottom attached rdm-sidebar"> <dl class="details-list"> <dt class="ui tiny header">Resource type</dt> <dd>Technical note</dd> <dt class="ui tiny header">Publisher</dt> <dd>CERN</dd> <dt class="ui tiny header">Languages</dt> <dd> English </dd> </dl> </div> </div> <div class="sidebar-container"> <h2 class="ui medium top attached header mt-0">Citation</h2> <div id="citation" class="ui segment bottom attached rdm-sidebar"> <div id="recordCitation" data-record='{"access": {"embargo": {"active": false, "reason": null}, "files": "public", "record": "public", "status": "open"}, "created": "2022-08-29T02:00:00+00:00", "custom_fields": {"cern:departments": [{"id": "BE", "title": {"en": "BE"}}]}, "deletion_status": {"is_deleted": false, "status": "P"}, "expanded": {"parent": {"access": {"owned_by": {"active": null, "blocked_at": null, "confirmed_at": null, "email": "", "id": "50701", "is_current_user": null, "links": {"avatar": "https://repository.cern/api/users/50701/avatar.svg"}, "profile": {"affiliations": "", "full_name": "Deleted user"}, "username": "Deleted user", "verified_at": null}}, "communities": {"default": {"access": {"review_policy": "members", "visibility": "public"}, "id": "479178e3-5db9-426b-be8c-4a33317098e3", "links": {"logo": "https://repository.cern/api/communities/479178e3-5db9-426b-be8c-4a33317098e3/logo"}, "metadata": {"description": null, "title": "Summer Student Programme", "type": null}, "slug": "summer-student-programme"}}}}, "files": {"count": 1, "enabled": true, "entries": {"cern_report_zsofia_adam.pdf": {"access": {"hidden": false}, "checksum": "md5:6e3b609bc7cffcf7c20d35a34fe726b5", "ext": "pdf", "id": "40bb8dc4-e32e-47f5-85d5-4ecf53b8c470", "key": "cern_report_zsofia_adam.pdf", "links": {"content": "https://repository.cern/api/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf/content", "iiif_api": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/full/0/default.png", "iiif_base": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf", "iiif_canvas": "https://repository.cern/api/iiif/record:rq11e-47p08/canvas/cern_report_zsofia_adam.pdf", "iiif_info": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/info.json", "self": "https://repository.cern/api/records/rq11e-47p08/files/cern_report_zsofia_adam.pdf"}, "metadata": {}, "mimetype": "application/pdf", "size": 538993, "storage_class": "L"}}, "order": [], "total_bytes": 538993}, "id": "rq11e-47p08", "is_draft": false, "is_published": true, "links": {"access": "https://repository.cern/api/records/rq11e-47p08/access", "access_grants": "https://repository.cern/api/records/rq11e-47p08/access/grants", "access_groups": "https://repository.cern/api/records/rq11e-47p08/access/groups", "access_links": "https://repository.cern/api/records/rq11e-47p08/access/links", "access_request": "https://repository.cern/api/records/rq11e-47p08/access/request", "access_users": "https://repository.cern/api/records/rq11e-47p08/access/users", "archive": "https://repository.cern/api/records/rq11e-47p08/files-archive", "archive_media": "https://repository.cern/api/records/rq11e-47p08/media-files-archive", "communities": "https://repository.cern/api/records/rq11e-47p08/communities", "communities-suggestions": "https://repository.cern/api/records/rq11e-47p08/communities-suggestions", "draft": "https://repository.cern/api/records/rq11e-47p08/draft", "files": "https://repository.cern/api/records/rq11e-47p08/files", "latest": "https://repository.cern/api/records/rq11e-47p08/versions/latest", "latest_html": "https://repository.cern/records/rq11e-47p08/latest", "media_files": "https://repository.cern/api/records/rq11e-47p08/media-files", "parent": "https://repository.cern/api/records/w59n1-asa87", "parent_html": "https://repository.cern/records/w59n1-asa87", "requests": "https://repository.cern/api/records/rq11e-47p08/requests", "reserve_doi": "https://repository.cern/api/records/rq11e-47p08/draft/pids/doi", "self": "https://repository.cern/api/records/rq11e-47p08", "self_html": "https://repository.cern/records/rq11e-47p08", "self_iiif_manifest": "https://repository.cern/api/iiif/record:rq11e-47p08/manifest", "self_iiif_sequence": "https://repository.cern/api/iiif/record:rq11e-47p08/sequence/default", "thumbnails": {"10": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^10,/0/default.jpg", "100": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^100,/0/default.jpg", "1200": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^1200,/0/default.jpg", "250": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^250,/0/default.jpg", "50": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^50,/0/default.jpg", "750": "https://repository.cern/api/iiif/record:rq11e-47p08:cern_report_zsofia_adam.pdf/full/^750,/0/default.jpg"}, "versions": "https://repository.cern/api/records/rq11e-47p08/versions"}, "media_files": {"count": 0, "enabled": false, "entries": {}, "order": [], "total_bytes": 0}, "metadata": {"additional_descriptions": [{"description": "Abbreviations: FRET - Formal Requirements Elicitation Tool", "type": {"id": "other", "title": {"de": "Sonstige", "en": "Other"}}}], "contributors": [{"person_or_org": {"family_name": "Borja Fern\u00e1ndez Adiego", "name": "Borja Fern\u00e1ndez Adiego", "type": "personal"}, "role": {"id": "supervisor", "title": {"de": "SupervisorIn", "en": "Supervisor"}}}], "creators": [{"person_or_org": {"family_name": "Adam", "given_name": "Zsofia", "identifiers": [{"identifier": "2807895", "scheme": "lcds"}], "name": "Adam, Zsofia", "type": "personal"}}], "description": "This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements.", "identifiers": [{"identifier": "CERN-STUDENTS-Note-2022-107", "scheme": "cds_ref"}], "languages": [{"id": "eng", "title": {"en": "English"}}], "publication_date": "2022-09-02", "publisher": "CERN", "resource_type": {"id": "publication-technicalnote", "title": {"de": "Technical Note", "en": "Technical note"}}, "subjects": [{"id": "Engineering", "scheme": "CERN", "subject": "Engineering"}, {"id": "Computing and Computers", "scheme": "CERN", "subject": "Computing and Computers"}, {"subject": "PLCVerif"}, {"subject": "PLC"}, {"subject": "Programmable Logic Controller"}, {"subject": "FRET"}, {"subject": "Requirement"}, {"subject": "Formal Methods"}, {"subject": "Formal Verification"}], "title": "Formulating Requirements with FRET for PLCVerif"}, "parent": {"access": {"owned_by": {"user": "50701"}, "settings": {"accept_conditions_text": null, "allow_guest_requests": false, "allow_user_requests": false, "secret_link_expiration": 0}}, "communities": {"default": "479178e3-5db9-426b-be8c-4a33317098e3", "entries": [{"access": {"member_policy": "open", "members_visibility": "public", "record_submission_policy": "closed", "review_policy": "members", "visibility": "public"}, "children": {"allow": false}, "created": "2024-12-03T14:34:24.553980+00:00", "custom_fields": {}, "deletion_status": {"is_deleted": false, "status": "P"}, "id": "479178e3-5db9-426b-be8c-4a33317098e3", "links": {}, "metadata": {"title": "Summer Student Programme", "website": "https://careers.cern/summer"}, "revision_id": 7, "slug": "summer-student-programme", "updated": "2024-12-16T08:40:06.380981+00:00"}], "ids": ["479178e3-5db9-426b-be8c-4a33317098e3"]}, "id": "w59n1-asa87", "pids": {}}, "pids": {"oai": {"identifier": "oai:oai:invenio-app-rdm.org::rq11e-47p08", "provider": "oai"}}, "revision_id": 9, "stats": {"all_versions": {"data_volume": 237695913.0, "downloads": 441, "unique_downloads": 372, "unique_views": 332, "views": 594}, "this_version": {"data_volume": 237695913.0, "downloads": 441, "unique_downloads": 372, "unique_views": 332, "views": 594}}, "status": "published", "ui": {"access_status": {"description_l10n": "The record and files are publicly accessible.", "embargo_date_l10n": null, "icon": "unlock", "id": "open", "message_class": "", "title_l10n": "Open"}, "additional_descriptions": [{"description": "Abbreviations: FRET - Formal Requirements Elicitation Tool", "type": {"id": "other", "title_l10n": "Other"}}], "contributors": {"affiliations": [], "contributors": [{"person_or_org": {"family_name": "Borja Fern\u00e1ndez Adiego", "name": "Borja Fern\u00e1ndez Adiego", "type": "personal"}, "role": {"id": "supervisor", "title": "Supervisor"}}]}, "created_date_l10n_long": "August 29, 2022", "creators": {"affiliations": [], "creators": [{"person_or_org": {"family_name": "Adam", "given_name": "Zsofia", "identifiers": [{"identifier": "2807895", "scheme": "lcds"}], "name": "Adam, Zsofia", "type": "personal"}}]}, "custom_fields": {"cern:departments": [{"id": "BE", "title_l10n": "BE"}]}, "description_stripped": "This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements.", "is_draft": false, "languages": [{"id": "eng", "title_l10n": "English"}], "publication_date_l10n_long": "September 2, 2022", "publication_date_l10n_medium": "Sep 2, 2022", "resource_type": {"id": "publication-technicalnote", "title_l10n": "Technical note"}, "updated_date_l10n_long": "January 28, 2025", "version": "v1"}, "updated": "2025-01-28T15:41:31.937890+00:00", "versions": {"index": 1, "is_latest": true}}' data-styles='[["apa", "APA"], ["harvard-cite-them-right", "Harvard"], ["modern-language-association", "MLA"], ["vancouver", "Vancouver"], ["chicago-fullnote-bibliography", "Chicago"], ["ieee", "IEEE"]]' data-defaultstyle='"apa"' data-include-deleted='false'> </div> </div> </div> <div class="sidebar-container"> <h2 class="ui medium top attached header mt-0">Export</h2> <div id="export-record" class="ui segment bottom attached exports rdm-sidebar"> <div id="recordExportDownload" data-formats='[{"export_url": "/records/rq11e-47p08/export/json", "name": "JSON"}, {"export_url": "/records/rq11e-47p08/export/json-ld", "name": "JSON-LD"}, {"export_url": "/records/rq11e-47p08/export/csl", "name": "CSL"}, {"export_url": "/records/rq11e-47p08/export/datacite-json", "name": "DataCite JSON"}, {"export_url": "/records/rq11e-47p08/export/datacite-xml", "name": "DataCite XML"}, {"export_url": "/records/rq11e-47p08/export/dublincore", "name": "Dublin Core XML"}, {"export_url": "/records/rq11e-47p08/export/marcxml", "name": "MARCXML"}, {"export_url": "/records/rq11e-47p08/export/bibtex", "name": "BibTeX"}, {"export_url": "/records/rq11e-47p08/export/geojson", "name": "GeoJSON"}, {"export_url": "/records/rq11e-47p08/export/dcat-ap", "name": "DCAT"}, {"export_url": "/records/rq11e-47p08/export/codemeta", "name": "Codemeta"}, {"export_url": "/records/rq11e-47p08/export/cff", "name": "Citation File Format"}]'></div> </div> </div> <section id="upload-info" role="note" aria-label="Upload information" class="sidebar-container ui segment rdm-sidebar text-muted" > <h2 class="ui small header text-muted p-0 mb-5"><small>Technical metadata</small></h2> <dl class="m-0"> <dt class="inline"><small>Created</small></dt> <dd class="inline"> <small>August 29, 2022</small> </dd> <div> <dt class="rel-mt-1 inline"><small>Modified</small></dt> <dd class="inline"> <small>January 28, 2025</small> </dd> </div> </dl> </section> </aside> </div> </div> <div class="ui container"> <div class="ui relaxed grid"> <div class="two column row"> <div class="sixteen wide tablet eleven wide computer column"> <div class="ui grid"> <div class="centered row rel-mt-1"> <button id="jump-btn" class="jump-to-top ui button labeled icon" aria-label="Jump to top of page"> <i class="arrow alternate circle up outline icon"></i> Jump up </button> </div> </div></div> </div> </div> </div> </div> </div> </main> <footer id="rdm-footer-element"> <footer id="rdm-footer-element"> <div class="footer-top"> <div class="ui container rel-pl-2 rel-pr-2"> <div class="ui grid"> <div class="rdm-footer five wide tablet three wide computer eight wide mobile column"> <h2 class="ui small header">About</h2> <p><a href="/about">About</a></p> <p><a href="https://cds-blog.web.cern.ch/">Blog</a></p> <p><a href="http://new-cds-project.docs.cern.ch/">Migration project</a></p> <p><a href="/privacy-notice">Privacy notice</a></p> </div> <div class="rdm-footer five wide tablet three wide computer eight wide mobile column"> <h2 class="ui small header">Help</h2> <p><a href="https://cern.service-now.com/service-portal?id=service_element&name=CDS-Service">CERN Service Now</a></p> </div> <div class="rdm-footer five wide tablet three wide computer eight wide mobile column"> <h2 class="ui small header">Other CDS websites</h2> <p><a href="https://videos.cern.ch">CDS Videos</a></p> <p><a href="https://catalogue.library.cern">CERN Library Catalogue</a></p> <p><a href="https://cds.cern.ch">Former CDS</a></p> </div> <div class="five wide tablet three wide computer eight wide mobile column right aligned right floated"> <img class="ui image small" src="/static/images/CERNLogo-White.svg" alt="CERN"/> </div> </div> </div> </div> </footer> <div class="footer-bottom sub-footer"> <div class="ui container"> <div class="ui grid"> <div class="eight wide column left middle aligned"> Powered by <a href="https://inveniosoftware.org/products/rdm">InvenioRDM</a> </div> <div class="eight wide column right aligned"> <ul class="ui inverted horizontal link list"> <li class="item"> <a href="/content-policy">Content policy</a> </li> <li class="item"> <a href="/preservation-policy">Preservation policy</a> </li> <li class="item"> <a href="/terms">Terms of Use</a> </li> </ul> </div> </div> </div> </div> </footer> <script type="text/javascript"> window.MathJax = { tex: { inlineMath: [['$', '$'], ['\$', '\$']], processEscapes: true // Allows escaping $ signs if needed } }; </script> <script type="text/javascript" src="//cdnjs.cloudflare.com/ajax/libs/mathjax/3.2.2/es5/tex-mml-chtml.js?config=TeX-AMS-MML_HTMLorMML"></script> <script src="/static/dist/js/manifest.ca1c2539201dcbfe91db.js"></script> <script src="/static/dist/js/73.c39079ca1fc2ae113347.js"></script> <script src="/static/dist/js/3526.cffc0a3bf3b7893f543c.js"></script> <script src="/static/dist/js/theme.df2465216f8b783a462f.js"></script> <script src="/static/dist/js/6671.3e933374bb287678e20d.js"></script> <script src="/static/dist/js/6506.11053731a380ad670d4c.js"></script> <script src="/static/dist/js/5373.4d3c97d870fcbcceede3.js"></script> <script src="/static/dist/js/8871.83bdb5bfed7707567078.js"></script> <script src="/static/dist/js/3692.f8494a9128a5283ac52b.js"></script> <script src="/static/dist/js/9300.a0444653c1720a08cc93.js"></script> <script src="/static/dist/js/9827.c60c224da4828a6e9bc8.js"></script> <script src="/static/dist/js/742.c9ff6bca3a608a9bce7d.js"></script> <script src="/static/dist/js/base-theme-rdm.159ec216daef09df0165.js"></script> <script src="/static/dist/js/i18n_app.99c66e0dc76dcd873a86.js"></script> <script src="/static/dist/js/278.31a4ac9c6c4c03bad263.js"></script> <script src="/static/dist/js/8102.8ca37a7a6650ce75a7fa.js"></script> <script src="/static/dist/js/overridable-registry.7ae1f161e88cfec4131e.js"></script> <script src="/static/dist/js/invenio-app-rdm-landing-page-theme.9b56690388e335810f04.js"></script> <script src="/static/dist/js/4709.afc06c31ef4490ce324b.js"></script> <script src="/static/dist/js/5941.416c32bce9b1f6137489.js"></script> <script src="/static/dist/js/5019.6ee301c738aee3dd0d87.js"></script> <script src="/static/dist/js/3272.5c119e32af15f0cc6cd6.js"></script> <script src="/static/dist/js/5368.1f7b03f1b2b6edbdbe27.js"></script> <script src="/static/dist/js/9945.e11a5a6ff50535c72070.js"></script> <script src="/static/dist/js/4838.efc973719d5b4e34931b.js"></script> <script src="/static/dist/js/1357.1a00892dcbfbc2ad0944.js"></script> <script src="/static/dist/js/1990.4198c9b3429de6dfebed.js"></script> <script src="/static/dist/js/1644.dbb0abfbd718407bcf0c.js"></script> <script src="/static/dist/js/8962.fe354ce623580a1b760d.js"></script> <script src="/static/dist/js/357.72be62380654f54fa647.js"></script> <script src="/static/dist/js/9562.7cc822b17dbf225c56dd.js"></script> <script src="/static/dist/js/5680.37299fa1f650e9b2e741.js"></script> <script src="/static/dist/js/invenio-app-rdm-landing-page.1c2042ae7f001b73fed9.js"></script> <script src="/static/dist/js/previewer_theme.77f20174699c7786038a.js"></script>  <script> var _paq = window._paq = window._paq || []; /* tracker methods like "setCustomDimension" should be called before "trackPageView" */ _paq.push(['trackPageView']); _paq.push(['enableLinkTracking']); (function() { var u="https://webanalytics.web.cern.ch/"; _paq.push(['setTrackerUrl', u+'matomo.php']); _paq.push(['setSiteId', '756']); var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0]; g.async=true; g.src=u+'matomo.js'; s.parentNode.insertBefore(g,s); })(); </script>  </body> </html>

CINXE.COM

Formulating Requirements with FRET for PLCVerif