Changes

              
    

          
          
        
        

            
f
1
{
f
1
{
            
2
  "author": "Weigl, Alexander",
2
  "author": "Weigl, Alexander",
            
3
  "author_email": "",
3
  "author_email": "",
            
4
  "creator_user_id": "17755db4-395a-4b3b-ac09-e8e3484ca700",
4
  "creator_user_id": "17755db4-395a-4b3b-ac09-e8e3484ca700",
            
5
  "doi": "10.35097/1537",
5
  "doi": "10.35097/1537",
            
6
  "doi_date_published": "2023",
6
  "doi_date_published": "2023",
            
7
  "doi_publisher": "",
7
  "doi_publisher": "",
            
8
  "doi_status": "True",
8
  "doi_status": "True",
            
9
  "groups": [],
9
  "groups": [],
            
10
  "id": "4dbf9cf7-f142-4bd2-89b4-b9ada972f657",
10
  "id": "4dbf9cf7-f142-4bd2-89b4-b9ada972f657",
            
11
  "isopen": false,
11
  "isopen": false,
            
12
  "license_id": "CC BY-NC-SA 4.0 
12
  "license_id": "CC BY-NC-SA 4.0 
            
13
Attribution-NonCommercial-ShareAlike",
13
Attribution-NonCommercial-ShareAlike",
            
14
  "license_title": "CC BY-NC-SA 4.0 
14
  "license_title": "CC BY-NC-SA 4.0 
            
15
Attribution-NonCommercial-ShareAlike",
15
Attribution-NonCommercial-ShareAlike",
            
16
  "metadata_created": "2023-08-04T08:51:00.231491",
16
  "metadata_created": "2023-08-04T08:51:00.231491",
            
t
17
  "metadata_modified": "2023-08-04T09:04:24.609840",
t
17
  "metadata_modified": "2023-08-04T09:31:29.255182",
            
18
  "name": "rdr-doi-10-35097-1537",
18
  "name": "rdr-doi-10-35097-1537",
            
19
  "notes": "Abstract: This archive contains the evaluation for 
19
  "notes": "Abstract: This archive contains the evaluation for 
            
20
\"Formal Specification and\r\nVerification for Automated Production 
20
\"Formal Specification and\r\nVerification for Automated Production 
            
21
Systems\". In particular, you\r\nfind evaluation environments for 
21
Systems\". In particular, you\r\nfind evaluation environments for 
            
22
Chapter 7 (Evaluation (PART I -\r\nGeneralized Test Tables)), 10 
22
Chapter 7 (Evaluation (PART I -\r\nGeneralized Test Tables)), 10 
            
23
(Relational Test Tables), 11 (Provably\r\nForgetting of Information), 
23
(Relational Test Tables), 11 (Provably\r\nForgetting of Information), 
            
24
and 12 (Modular Regression Verification).\r\n\r\nFor more details, 
24
and 12 (Modular Regression Verification).\r\n\r\nFor more details, 
            
25
refer to the READMEs of the individual 
25
refer to the READMEs of the individual 
            
26
sub-folders.\r\nTechnicalRemarks: 
26
sub-folders.\r\nTechnicalRemarks: 
            
27
--------------------------------------------------------------\r\n\r\n     
27
--------------------------------------------------------------\r\n\r\n     
            
28
Formal Specification and Verification for Automated Production 
28
Formal Specification and Verification for Automated Production 
            
29
Systems\r\n\r\n                                Alexander Weigl\r\n\r\n                              
29
Systems\r\n\r\n                                Alexander Weigl\r\n\r\n                              
            
30
COMPANTION MATERIAL\r\n                              
30
COMPANTION MATERIAL\r\n                              
            
31
------------------------------------------------------\r\n\r\n\r\nThis 
31
------------------------------------------------------\r\n\r\n\r\nThis 
            
32
bundle contains companion material for the PhD thesis 
32
bundle contains companion material for the PhD thesis 
            
33
\"Formal\r\nSpecification and Verification for Automated Production 
33
\"Formal\r\nSpecification and Verification for Automated Production 
            
34
Systems\". In\r\nparticular you find following items:\r\n\r\n1. Files 
34
Systems\". In\r\nparticular you find following items:\r\n\r\n1. Files 
            
35
of the evaluation of the chapters:\r\n   * Chapter 07: Evaluation 
35
of the evaluation of the chapters:\r\n   * Chapter 07: Evaluation 
            
36
(PART I - Generalized Test Tables)\r\n   * Chapter 10: Relational Test 
36
(PART I - Generalized Test Tables)\r\n   * Chapter 10: Relational Test 
            
37
Tables\r\n   * Chapter 11: Provably Forgetting of Information\r\n   * 
37
Tables\r\n   * Chapter 11: Provably Forgetting of Information\r\n   * 
            
38
Chapter 12: Modular Regression Verification\r\n   \r\n   Runtime 
38
Chapter 12: Modular Regression Verification\r\n   \r\n   Runtime 
            
39
artefacts and log files are included.\r\n   \r\n   Further details are 
39
artefacts and log files are included.\r\n   \r\n   Further details are 
            
40
given in the `README.md` files of the\r\n   sub-directories.\r\n   
40
given in the `README.md` files of the\r\n   sub-directories.\r\n   
            
41
\r\n2. Software for the evaluation\r\n   * `verifaps-lib`: the 
41
\r\n2. Software for the evaluation\r\n   * `verifaps-lib`: the 
            
42
developed library for the verification of automated\r\n     production 
42
developed library for the verification of automated\r\n     production 
            
43
systems (GPL v3)\r\n   * `eldarica`: used for verification of C files 
43
systems (GPL v3)\r\n   * `eldarica`: used for verification of C files 
            
44
(BSD 3-clause license)\r\n   * `ic3ia`: used for the of VMT files 
44
(BSD 3-clause license)\r\n   * `ic3ia`: used for the of VMT files 
            
45
(generated by `nuXmv`) (GPL v3)\r\n\r\n   Not included and required 
45
(generated by `nuXmv`) (GPL v3)\r\n\r\n   Not included and required 
            
46
for some experiments are\r\n   \r\n   * 
46
for some experiments are\r\n   \r\n   * 
            
47
[`nuXmv`](https://nuxmv.fbk.eu) (Version: 1.1.1, and 2.0.0),\r\n     
47
[`nuXmv`](https://nuxmv.fbk.eu) (Version: 1.1.1, and 2.0.0),\r\n     
            
48
model checker, not included due to license restrictions.\r\n   * 
48
model checker, not included due to license restrictions.\r\n   * 
            
49
[`SeaHorn`](https://seahorn.github.io/), \r\n     C program verifier, 
49
[`SeaHorn`](https://seahorn.github.io/), \r\n     C program verifier, 
            
50
not included due to its large space size\r\n \r\n     `SeaHorn` can be 
50
not included due to its large space size\r\n \r\n     `SeaHorn` can be 
            
51
easly obtained by Docker or Podman:\r\n     \r\n     ``` \r\n     $ 
51
easly obtained by Docker or Podman:\r\n     \r\n     ``` \r\n     $ 
            
52
podman run -ti seahorn/seahorn-llvm10:nightly\r\n     ```",
52
podman run -ti seahorn/seahorn-llvm10:nightly\r\n     ```",
            
53
  "num_resources": 0,
53
  "num_resources": 0,
            
54
  "num_tags": 8,
54
  "num_tags": 8,
            
55
  "orcid": "0000-0001-8446-4598",
55
  "orcid": "0000-0001-8446-4598",
            
56
  "organization": {
56
  "organization": {
            
57
    "approval_status": "approved",
57
    "approval_status": "approved",
            
58
    "created": "2023-01-12T13:30:23.238233",
58
    "created": "2023-01-12T13:30:23.238233",
            
59
    "description": "RADAR (Research Data Repository) is a 
59
    "description": "RADAR (Research Data Repository) is a 
            
60
cross-disciplinary repository for archiving and publishing research 
60
cross-disciplinary repository for archiving and publishing research 
            
61
data from completed scientific studies and projects. The focus is on 
61
data from completed scientific studies and projects. The focus is on 
            
62
research data from subjects that do not yet have their own 
62
research data from subjects that do not yet have their own 
            
63
discipline-specific infrastructures for research data management. ",
63
discipline-specific infrastructures for research data management. ",
            
64
    "id": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
64
    "id": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
            
65
    "image_url": "radar-logo.svg",
65
    "image_url": "radar-logo.svg",
            
66
    "is_organization": true,
66
    "is_organization": true,
            
67
    "name": "radar",
67
    "name": "radar",
            
68
    "state": "active",
68
    "state": "active",
            
69
    "title": "RADAR",
69
    "title": "RADAR",
            
70
    "type": "organization"
70
    "type": "organization"
            
71
  },
71
  },
            
72
  "owner_org": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
72
  "owner_org": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
            
73
  "private": false,
73
  "private": false,
            
74
  "production_year": "2021",
74
  "production_year": "2021",
            
75
  "publication_year": "2023",
75
  "publication_year": "2023",
            
76
  "publishers": [
76
  "publishers": [
            
77
    {
77
    {
            
78
      "publisher": "Karlsruhe Institute of Technology"
78
      "publisher": "Karlsruhe Institute of Technology"
            
79
    }
79
    }
            
80
  ],
80
  ],
            
81
  "relationships_as_object": [],
81
  "relationships_as_object": [],
            
82
  "relationships_as_subject": [],
82
  "relationships_as_subject": [],
            
83
  "repository_name": "RADAR (Research Data Repository)",
83
  "repository_name": "RADAR (Research Data Repository)",
            
84
  "resources": [],
84
  "resources": [],
            
85
  "services_used_list": "",
85
  "services_used_list": "",
            
86
  "source_metadata_created": "2023",
86
  "source_metadata_created": "2023",
            
87
  "source_metadata_modified": "",
87
  "source_metadata_modified": "",
            
88
  "state": "active",
88
  "state": "active",
            
89
  "subject_areas": [
89
  "subject_areas": [
            
90
    {
90
    {
            
91
      "subject_area_additional": "",
91
      "subject_area_additional": "",
            
92
      "subject_area_name": "Computer Science"
92
      "subject_area_name": "Computer Science"
            
93
    }
93
    }
            
94
  ],
94
  ],
            
95
  "tags": [
95
  "tags": [
            
96
    {
96
    {
            
97
      "display_name": "Automated Production Systems",
97
      "display_name": "Automated Production Systems",
            
98
      "id": "3558d431-6403-42a4-8a49-85d39e4ec50d",
98
      "id": "3558d431-6403-42a4-8a49-85d39e4ec50d",
            
99
      "name": "Automated Production Systems",
99
      "name": "Automated Production Systems",
            
100
      "state": "active",
100
      "state": "active",
            
101
      "vocabulary_id": null
101
      "vocabulary_id": null
            
102
    },
102
    },
            
103
    {
103
    {
            
104
      "display_name": "Eldarica",
104
      "display_name": "Eldarica",
            
105
      "id": "108d0d92-9c22-4694-97bf-ed4b8caea61d",
105
      "id": "108d0d92-9c22-4694-97bf-ed4b8caea61d",
            
106
      "name": "Eldarica",
106
      "name": "Eldarica",
            
107
      "state": "active",
107
      "state": "active",
            
108
      "vocabulary_id": null
108
      "vocabulary_id": null
            
109
    },
109
    },
            
110
    {
110
    {
            
111
      "display_name": "Formal Specification",
111
      "display_name": "Formal Specification",
            
112
      "id": "bfb1fa6d-c025-458a-a7a6-c1420d751f46",
112
      "id": "bfb1fa6d-c025-458a-a7a6-c1420d751f46",
            
113
      "name": "Formal Specification",
113
      "name": "Formal Specification",
            
114
      "state": "active",
114
      "state": "active",
            
115
      "vocabulary_id": null
115
      "vocabulary_id": null
            
116
    },
116
    },
            
117
    {
117
    {
            
118
      "display_name": "Formal Verification",
118
      "display_name": "Formal Verification",
            
119
      "id": "179c2fd3-2973-4900-860b-d53e7d813ef4",
119
      "id": "179c2fd3-2973-4900-860b-d53e7d813ef4",
            
120
      "name": "Formal Verification",
120
      "name": "Formal Verification",
            
121
      "state": "active",
121
      "state": "active",
            
122
      "vocabulary_id": null
122
      "vocabulary_id": null
            
123
    },
123
    },
            
124
    {
124
    {
            
125
      "display_name": "IC3",
125
      "display_name": "IC3",
            
126
      "id": "026a566a-a9da-4869-818d-7d67c5e03e7b",
126
      "id": "026a566a-a9da-4869-818d-7d67c5e03e7b",
            
127
      "name": "IC3",
127
      "name": "IC3",
            
128
      "state": "active",
128
      "state": "active",
            
129
      "vocabulary_id": null
129
      "vocabulary_id": null
            
130
    },
130
    },
            
131
    {
131
    {
            
132
      "display_name": "Manufacturing Systems",
132
      "display_name": "Manufacturing Systems",
            
133
      "id": "22a7c445-d899-49fb-8afa-acb46ea8b203",
133
      "id": "22a7c445-d899-49fb-8afa-acb46ea8b203",
            
134
      "name": "Manufacturing Systems",
134
      "name": "Manufacturing Systems",
            
135
      "state": "active",
135
      "state": "active",
            
136
      "vocabulary_id": null
136
      "vocabulary_id": null
            
137
    },
137
    },
            
138
    {
138
    {
            
139
      "display_name": "SeaHorn",
139
      "display_name": "SeaHorn",
            
140
      "id": "ee97fb24-adc0-4523-8ffd-97458b9c2c95",
140
      "id": "ee97fb24-adc0-4523-8ffd-97458b9c2c95",
            
141
      "name": "SeaHorn",
141
      "name": "SeaHorn",
            
142
      "state": "active",
142
      "state": "active",
            
143
      "vocabulary_id": null
143
      "vocabulary_id": null
            
144
    },
144
    },
            
145
    {
145
    {
            
146
      "display_name": "nuXmv",
146
      "display_name": "nuXmv",
            
147
      "id": "c949182e-020f-4b56-8a66-6c84497e0e6f",
147
      "id": "c949182e-020f-4b56-8a66-6c84497e0e6f",
            
148
      "name": "nuXmv",
148
      "name": "nuXmv",
            
149
      "state": "active",
149
      "state": "active",
            
150
      "vocabulary_id": null
150
      "vocabulary_id": null
            
151
    }
151
    }
            
152
  ],
152
  ],
            
153
  "title": "Companion material for the phd thesis \"formal 
153
  "title": "Companion material for the phd thesis \"formal 
            
154
specification and verification for automated production systems\"",
154
specification and verification for automated production systems\"",
            
155
  "type": "vdataset",
155
  "type": "vdataset",
            
156
  "url": "https://doi.org/10.35097/1537"
156
  "url": "https://doi.org/10.35097/1537"
            
157
}
157
}