-
Notifications
You must be signed in to change notification settings - Fork 1
/
project_requirements.lando
106 lines (90 loc) · 4.37 KB
/
project_requirements.lando
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
// Copyright 2021, 2022, 2023 Galois, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// All requirements that the RTS system must fulfill, as driven by the
// IEEE 603-2018 standards and the NRC RFP.
requirements HARDENS Project High-level Requirements
// The high-level requirements for the project stipulated by the NRC RFP.
NRC Understanding
Provide to the NRC expert technical services in order to develop a
better understanding of how Model-Based Systems Engineering (MBSE)
methods and tools can support regulatory reviews of adequate design
and design assurance.
Identify Regulatory Gaps
Identify any barriers or gaps associated with MBSE in a regulatory
review of Digital Instrumentation and Control Systems for existing
Nuclear Power Plants.
Demonstrate
Galois will demonstrate to the Nuclear Regulatory Commission (NRC)
cutting-edge capabilities in the model-based design, validation, and
verification of safety-critical, mission-critical, high-assurance
systems.
Demonstrator Parts
Our demonstrator includes high-assurance software and hardware,
includes open source RISC-V Central Processing Units.
Demonstrator Groundwork
Our demonstrator lays the groundwork for a high-assurance reusable
product for safety critical Digital Instrumentation and Control
Systems systems in Nuclear Power Plants.
requirements NRC Characteristics
// The requirements driven by the IEEE 603-2018 standard for NPP I&C
// systems.
// Both formal and rigorous consistency checks of the requirements
// will be accomplished by using false theorem checks and proofs in
// the Cryptol model and in software and hardware source code;
Requirements Consistency
Requirements must be shown to be consistent.
// A rigorous completeness validation of the requirements will be
// accomplished by demonstrating traceability from the project
// specification (including the RFP text describing the reactor trip
// system) to the formal models of the system and its properties.
Requirements Colloquial Completeness
The system must be shown to fulfill all requirements.
// A formal verification of completeness of the requirements will be
// accomplished by using the chosen requirements checking tool
Requirements Formal Completeness
Requirements must be shown to be formally complete.
// This characteristic will be demonstrated architecturally via the
// decoupling of computation across the two RISC-V instrumentation
// cores and two instrumentation units running on the FPGA.
Instrumentation Independence
Independence among the four divisions of instrumentation (inability
for the behavior of one division to interfere or adversely affect the
performance of another).
// This characteristic will be demonstrated architecturally by
// decoupling the compute and I/O channels of the units from one
// another.
Channel Independence
Independence among the two instrumentation channels within a division
(inability for the behavior of one channel to interfere or adversely
affect the performance of another).
// This characteristic will be demonstrated architecturally by
// partitioning the actuation logic across software and hardware
// units.
Actuation Independence
Independence among the two trains of actuation logic (inability for
the behavior of one train to interfere or adversely affect the
performance of another).
// This characteristic will be demonstrated by rigorous validation via
// runtime verification and formal verification of the model and its
// implementation, as discussed in detail below.
Actuation Correctness
Completion of actuation whenever coincidence logic is satisfied or
manual actuation is initiated.
// This characteristic will be demonstrated architecturally by
// partitioning the actuation logic across software and hardware
// units.
Self-Test/Trip Independence
Independence between periodic self-test functions and trip functions
(inability for the behavior of the self-testing to interfere or
adversely affect the trip functions).