The growing complexity of aerospace cyber-physical systems demands rigorous methods to ensure software correctness, reliability, and compliance with safety standards. Traditional verification techniques often fail to detect dimensional inconsistencies that can lead to critical failures. This paper presents a formal verification approach based on dimensional analysis, specifically tailored for aerospace software. The method employs mathematical models derived from the statistical characteristics of C/C++ source code to identify dimensional defects in computations, data flows, and control algorithms. The proposed approach provides several benefits: early compile-time detection of defects, reduced testing effort and duration, cost savings through the elimination of latent defects, and improved software reliability, robustness, and performance. By integrating dimensional analysis with formal specification and verification frameworks, the method enables early detection of inconsistencies and mitigates defect propagation across system components. Case studies show that the method detects up to 90% (with an average of 66%) of incorrect uses of software variables and operations at both compile time and run time. This detection rate depends on the distribution of operations and dimensions in the C++ source files. The results demonstrate the method's effectiveness in uncovering errors overlooked by conventional testing. Overall, the proposed technique serves as a complementary tool for aerospace software verification, enhancing quality assurance and supporting certification processes.
Aerospace cyber-physical systems (CPS) are highly integrated environments where physical processes such as flight dynamics are tightly coupled with computational algorithms, sensors, actuators, and control systems [1]. These systems are increasingly central to modern aerospace engineering, improving efficiency, safety, performance, and real-time decision-making.
Applications of aerospace CPS span autonomous aircraft, spacecraft and satellites, commercial and military aviation, and predictive maintenance. In these contexts, CPS enable autonomy, advanced flight control, digital twins, sensor fusion, and adaptive diagnostics [2].
Despite their advantages, aerospace CPS face several critical challenges. Real-time constraints demand processing of large volumes of sensor data with strict latency requirements, especially for navigation, flight control, and emergency response. Safety and reliability are paramount, as these systems are safety-critical and must be fault-tolerant and resilient to avoid catastrophic failures. Integration and testing also remain complex, requiring approaches such as model-based design (MBD) to ensure subsystem interoperability [3]. Finally, increasing reliance on digital communication exposes aerospace CPS to cybersecurity threats, necessitating robust protection mechanisms[4].
Addressing these challenges necessitates advanced verification methods. Classical approaches to software verification, including Hoare’s seminal work on proving compiler correctness [5], demonstrate that formal verification can provide guarantees about program behavior beyond syntactic correctness [6]. Building on these principles, this paper explores the use of formal verification [7] based on dimensional analysis (DA) [8] as a novel approach to enhance the reliability and safety of aerospace CPS software. Prior work by the authors [9] [10] has demonstrated the feasibility of applying DA to C/C++ code for detecting latent errors and ensuring physical consistency.
This paper explores the use of formal verification based onDA as a novel approach to improve the reliability and safety of aerospace CPS software.
The proposed approach leverages natural software invariants, defined as the physical dimensions of variables corresponding to real-world quantities. By integrating these invariants into program specifications, program expressions can be reformulated into a set of lemmas requiring formal proof. This process enables verification of both dimensional homogeneity and program conciseness.
As noted by Martínez-Rojas et al. [11], DA is a well-established methodology in physics and engineering, used to identify or validate relationships among physical quantities based on their dimensions. Within the International System of Units (SI) [12], each physical quantity is expressed as a combination of seven base dimensions: length (meter, m), time (second, s), amount of substance (mole, mol), electric current (ampere, A), temperature (kelvin, K), luminous intensity (candela, cd), and mass (kilogram, kg) [13]. Derived units are defined as products of powers of base units, and when the numerical factor of such a product equals one, they are classified as coherent derived units. Together, SI base and coherent derived units form a coherent system, where equations involving numerical values mirror the structure of the underlying physical relationships. This property ensures consistency and accuracy in computations involving physical quantities, making DA a reliable foundation for software verification.
Some coherent derived units in the SI are assigned specific names and, together with the seven base units, form the foundation of the SI system. All other units are expressed as combinations of these. The central principle of DA is that physical laws must remain valid regardless of the units used. According to the rule of dimensional homogeneity, every physically meaningful equation must balance dimensions on both sides. This principle underpins the use of DA across physics and engineering.
Conventional software analysis tools primarily check syntax and semantics, but not the physical correctness of code. When program code is treated as a set of expressions involving variables, constants, and operations, DA can be integrated into the compilation or verification process. This enables the detection of mismatches in variable usage, inconsistent unit conversions, and incorrect dimensional operations directly at the software level. By embedding dimensional checks into program specifications, aerospace and safety-critical applications can benefit from early error detection, reduced defect propagation, and improved reliability of C/C++ implementations [14].
The correctness of program expressions can be evaluated by analyzing the dimensionality of their values. When expressions preserve dimensional homogeneity, they are likely to represent physically meaningful relationships. Conversely, violations of homogeneity signal incorrect use of program variables or operations. Unlike conventional checks, DA can be applied not only to simple expressions but also to procedure and function calls, enabling a broader validation of software behavior.
DA thus provides a systematic way to ensure the physical correctness of software code. By embedding physical dimensions into program specifications, it becomes possible to verify that computations remain consistent with the physical laws governing the modeled system. In this view, software can be regarded as a model of a physical process, and DA serves as a validation tool to confirm the model’s adherence to physical principles.
Incorporating DA into the software development and verification process enables the detection of errors caused by inconsistent or incorrect unit usage [15]. This contributes to the development of safer, more reliable, and physically accurate software—particularly in safety-critical domains such as aerospace cyber-physical systems.
A software system can be viewed as a hierarchy of interacting components. At the highest level, it is composed of subsystems; each subsystem consists of software units, and each unit is defined by a set of operators. Operators, in turn, are expressed as ordered sequences of statements or expressions. This hierarchical structure allows systematic verification of interactions and operations across different levels of the system.
To establish dimensional homogeneity within the system, verification must proceed step by step: the homogeneity of the overall system depends on the homogeneity of its subsystems; each subsystem’s homogeneity depends on that of its software units; and unit-level homogeneity requires the homogeneity of individual statements or expressions. This layered approach provides a structured pathway for verifying dimensional consistency throughout the code.
Within this framework, we distinguish between two categories of operations. Multiplicative operations (*, /, etc.) generate new physical dimensions, while additive operations (+, −, =, <, ≤, >, ≥, !=, etc.) act as checkpoints, enforcing dimensional homogeneity. When program variables are associated with specific physical dimensions, this property can be treated as a software invariant. Each additive operation then serves as a basis for generating lemmas, which collectively support the formal verification of dimensional correctness across the system.
DA enables verification of the physical dimensions of program variables, allowing the detection of errors caused by inconsistent unit usage, incorrect dimensional relationships, or improper application of operations, variables, and procedures. Nonetheless, challenges arise when different quantities share the same dimensions. For example, moments of inertia and angular velocity both involve combinations of mass and length, yet represent fundamentally different physical concepts. Detecting defects in such cases requires careful analysis of expressions.
Software defect detection models designed to identify errors, inconsistencies, and potential faults in software systems before deployment. These models aim to predict, locate, and prevent defects by analyzing code structure, execution patterns, or software behavior.
Proposed defect detection models incorporate probabilistic methods to improve predictive accuracy, leveraging defect data. In safety-critical domains, such as aerospace and automotive systems, defect detection models are essential for ensuring reliability and compliance with dimensional homogeneity. 3.1. General Software Defect Detection Model To simplify the analysis, we assume that each software statement may contain at most one defect, occurring with a probability of Pdef. The model begins with the initial state labeled “Software”, which branches into two possible outcomes: “Software has a defect” with probability Pdef, and “Software does not have a defect” with probability 1− Pdef.
Decision trees provide a structured way to visualize sequences of decisions or events along with their probabilities and outcomes. In the context of software defect detection, they can be enhanced by incorporating DA. By assigning physical dimensions as invariants to program variables, DA allows the detection of defects arising from inconsistent or incorrect use of units and operations. Each node in the decision tree can represent not only the presence or absence of a syntactic or semantic defect but also violations of dimensional homogeneity.
This combined approach enables early identification of errors that might remain undetected by conventional testing. For example, a branch could represent a statement where a variable’s dimensional type conflicts with an operation, triggering a defect detection alert. Figure 1 illustrates a decision tree model for software defect detection enhanced with dimensional analysis, demonstrating how this methodology supports systematic verification of both traditional and physics-based software correctness.
Software has N software units. In the state ‘Software Uniti has a defect’, our focus shifts to detecting the defect. The model branches out into two possible outcomes: ‘Defect detected’ and ‘Defect not detected’, with probabilities of PDD and 1− PDD, respectively. Let us define that software units has equal Pdef Here Pdef represents a probability of a software defect in the code. The conditional probability of software uniti defect detection defined as: ηi=
Pdef PDDi+ Pdef (1− PDDi) = PDDi .
(
By distinguishing these defect types, the model provides a more detailed representation of potential errors in software statements, enabling targeted detection and analysis. Despite the increased complexity, the assumption of a single defect per statement simplifies the probabilistic modeling, allowing the systematic application of decision tree methods and, when integrated with DA, facilitates the detection of both conventional coding errors and violations of physical correctness.
In this more complex model, the initial event state is ‘Software uniti.’ At the branching point, the model expands into two possible outcomes: ‘Variable’ and ‘Operation,’ with probabilities of Pvari and 1− Pvari, respectively which defined for every software uniti. The ‘Variable’ state has two potential outcomes at the next level: ‘Correct use of variable’ and ‘Incorrect use of variable’, with probabilities of 1− Pdef and Pdef, respectively. The ‘Incorrect use of variable’ state has two possible outcomes at the next level: ‘Variable defect detected’ and ‘Variable defect not detected’, with probabilities of PVDI and 1− PVDI , respectively. Here, PVDI represents the probability of detecting a variable defect in the uniti.
In addition to the ‘Variable’ state, the model also has an ‘Operation’ state, which has two possible outcomes at the next level: ‘Correct use of operation’ and ‘Incorrect use of operation’, with probabilities of 1− Pdef and Pdef, respectively.
The ‘Incorrect use of operation’ state has two possible outcomes: ‘Operation defect detected’ and ‘Operation defect not detected’, with probabilities of PODi and 1− PODi, respectively. Here, PODi represents the probability of detecting an operation defect in the source code of software uniti. The conditional probability of a software defect in software uniti can be defined as follows: ηi=
,
here PVDDi= Pvari Pdef PVDi, PODDi=(1− Pvari) Pdef PODi,
PVDNDi= Pvari Pdef (1− PVDi), PODNDi=(1− Pvari) Pdef (1− PODi)
and we have:
ηi= Pvari PVDi+(1− Pvari) PODi
(
,
As per Expression (
The total conditional probability of a software defect in software which includes N unit can be
N N defined as follows: η=∑ η ω =∑ ( Pvari PVDi+(1− Pvari) PODi) ωi , where ωi is a weight of i i i=1 i=1
N vi+ N Oi ∑ ( N vk + N Ok ) k=1 where N vi - number of variable used in software uniti, N Oi - - number of operation used in software uniti, N - total number of software units.
We can determine the value of Pvari, N vi, N Oi by analyzing the software code statically, i.e., without executing the code. However, to determine the values of PVDi and PODi, we would need to build additional software defect detection models. 3.2. Software Defect Detection Model for Incorrect Variable Usage.
The proposed model allows the detection of incorrect variable usage (see Figure 3).
This model has an initial state of ‘Software Variablei’ and is applied to each software unit. The initial state has two transitions to states ‘OK’ and ‘Check Dimension’, with probabilities 1− Pdef and Pdef, respectively. In the state ‘Check Dimension’, we can evaluate the required physical dimension of the variable using dimensional analysis.
If the actual physical dimension is equal to the required physical dimension, we cannot detect the software defect. However, if the dimensions differ, a software defect can be identified. In this case, the probabilities are Pdimi and 1− Pdimi, where Pdimi represents the probability that two randomly selected variables in software unit have the same physical dimension.
Let us define the conditional probability of defect detection of incorrect use of a program variable in the software uniti as follows:
PVDi=
PDDi+ PDNDi . var1 var2 var3 var 4 var5 var6
⋮ var Nvi−1 0 var Nvi ni11 ni21 0 0 0 0 ⋮ 0 ni31 0 0 0 0 ⋮ 0 0
Let us consider a set of distinct software variables {var1 , ... , var Nvi } and a set of diverse physical
dimensions {dim1 , ... , dimNdi }, where N vi represents the cardinality of set {vari } and N Di
represents the cardinality of set {dimi }. To depict the relationship between these variables and
dimensions, we can make use of an nijk-matrix (
The equation for the total number of usages of all software variables with dimension j in
software unit i can be written as follows:
where nikj represents the total number of usages of k-variable which has a j-physical dimension
which used in the i-unit; N vi is the cardinality set of software variables in the i-unit. Equation (
To define the probability of choosing l-variable and m-variable with the same dimensions, we can use the total number of usages of variables with the j-physical dimension and the total number of usages of all variables in the i-unit code:
According to (
Pdimi= ∑NVi ∑NDi ( nilm l=1 m=1 N VARi here nikj represents the number of usages for the k-variable with the j-physical dimension in the iunit; N VARi represents the total number of variable usages in the i-unit; N Di represents the total number of different dimensions of variables in the i-unit; and N Vi represents the total number of variables in the code.
The total conditional probability of software defect detection in a system consisting of N units
N can be defined as follows:ηD=∑ PVDi ωi , where PVDi=1− Pdimi , ωi is a weight of software i-unit i=1 ωi= NN vi , where N vi - number of variable usages in i-unit, N - total number of software units ∑ N vk k=1
P A + PM + PO=1.
Let us defineP A, PM, and PO as follows: (9) (10) (11)
N ηD=∑ (1− Pdimi) ωi.
i=1
Expression (9) defines the total conditional probability of detecting a software defect in software comprising N units. 3.3. Model for Detecting Incorrect Usage of Operations and Variables. Consider three subsets of C/C++ operations:
Additive operations (A) include arithmetic, assignment, comparison, increment/decrement, member access, and concatenation operators.
Multiplicative operations (M) include multiplication, division, modulo, and their compound assignment forms.
Other operations (O) cover logical, bitwise, shift, scope, conditional, and compound assignment operators not included in A or M.
This classification supports dimensional analysis by distinguishing operators that generate new dimensions (multiplicative) from those that check or preserve dimensional homogeneity (additive), while other operators are treated separately for consistency checks. In addition, we are given three probabilities associated with the utilization of this operation in the source code, namely, P A, PM, and PO. let us define the sum of these probabilities as the full group probability:
Here, N A represents the total number of “additive” operations in a file, N M represents the total number of “multiplicative” operations in a file, and N O represents the total number of “other” operations in the file.
In this case, we can build a decision tree for the detection of incorrect use of operations based on dimensional analysis. The model allows us to define the conditional probability of operation defect detection (see Figure 4).
According to Figure 4, the model begins with an initial state Operation, which branches into three additional states: A, M, and O, as defined in Expressions (10). TheM state further splits into two states: IMi (incorrect M operation, with probability PdefO) and CMi (correct M operation, with probability 1− PdefO). The CMi state then divides into CMVi (correct M operation with a Variable defect, probability Pdefv) and CVi (correct M operation with a correct variable, probability 1− Pdefv). The CMVi state expands further into two cases: CMVDNDi (correct M operation with an incorrect variable of the same dimension, probability Pdimi, defect not detected) and CMVDDi (correct M operation with an incorrect variable of a different dimension, probability 1− Pdimi, defect detected). Other nodes of the proposed model follow the same structural logic and are defined with analogous probability values.
Let us define theprobability of a software defect as Pdef= N NO+deNf v . where N def= N defO+ N defV is the total number of incorrect usages of operations and variables, and N O+ N v is the total number usages of operations and variables. That is why we can define the probabilities of a software defect as: PdefO= NNdeOfO , Pdefv= NNdevfv .
Because most operations have two operands, we can define that2 N O= N v and: Pdef=
NNdeOfO++2NNdOefV = 32 Pdefv + 32 NNdevfO .
3 PdefO≈3 Pdef, Pdefv≈ 2 Pdef.
According to Figure 4: N defV ≪1 3 N O 23NNdevfO ≪1 Pdef≈ P3defO ≈ 32 Pdefv, the conditional probability of software defect detection in the i-th unit can be defined as: ηi= formal verification can bedefinedas: φi=
∑ PDD ; ∑ PDD +∑ PDND the conditional probability of absence of software defects in the i-th unit after performing ∑ PDD +∑ POK .
∑ PDD +∑ PDND +∑ POK According (10) we have: ηi=1+
∑ PDND and φi=1−∑ PDND.
1−∑ POK
According to Figure 4: POK = PCOVOK + PCAVOK + PCMVOK, PDND= PCOVDND+ POODND+ PCAVDND+ P AADND+ PCMVDND+ P AAVDND
After simplificationPOK =1− 32 Pdef−3 Pdef + 92 P2def, ∑ PDND= 32 (1−3 Pdef) Pdef Pdim+3 PO2 Pdef +3 Pdef P2A (1− 32 Pdef)+ 92 P2A P2def Pdim.
Because Pdef ≪1 we can define: φi≈1−3 ( Pdim + PO2+ P2A ) Pdef,
2 ηi=1− 34 ( P2dim + PO2+ P2A ). (12) 1,2 0,8 0,6 0,4 0,2
0
The results of statistical modeling of conditional probabilities were obtained for Pdim=0,0001…0,1 and Pdef=0,00001…0,01, PO∈[ 0 …1], P A ∈[ PO …1], and are shown in Figures 5, 6, 7.
1,00E-05 0,0001 0,01
0,1 0,001 Pdim
The conditional probability of software defect detection is defined by the probabilities PO and PM. The average probability is approximately 0,66, with a minimum value of 0,26 and a maximum value of 1.0.
1,005
1 0,995 0,99 0,985 0,98 0,975 0,97 0,965 0,96 0,955 0,95 1,00E-06 1,00E-05
The average probability of software correctness after formal verification for Pdim=0,0001 is approximately 1 when Pdef varies within the range 0,000001…0,001.
1,005
1 0,995 0,99 0,985 0,98 0,975 0,97 0,965 0,96 0,955 0,95 1,00E-06 1,00E-05 0,001
0,01
The average probability of software correctness after formal verification for Pdim=0,01 is approximately 1 when Pdef varies within the range 0,000001…0,001.
The overall expected conditional probability of detecting dimensional defects in software.
η η=∑ i , where N Oi - total number of operations in the i-software unit.
i N Oi The overall expected conditional probability of correctness after formal verificationφ=∑ φi . i N Oi
If all software units contain the same number of operations, the total probability is defined by expressions (12) and (13). For units of different sizes, the resulting probabilities decrease.
This paper has introduced a formal software verification method that leverages software invariants derived from dimensional analysis. According to [10], a formal type system defines software templates based on physical dimensions and fundamental numerical types. These templates enable the creation of dimensioned constants and variables and support operator overloading in C++. According to the C++, it is also possible to define numeric literals as constants of different dimension types.
The proposed approach offers several notable advantages. It enables early defect detection at compile-time, which helps reduce the likelihood of error propagation into later development stages. It also decreases testing overhead by supporting formal verification during both compiletime and run-time. As a result, development costs are lowered because early identification of defects minimizes the need for extensive debugging, maintenance, and post-release corrections. The method enhances software quality, demonstrating the capability to detect between 60% and 90% of latent defects related to incorrect use of physical dimensions in software variables and improper application of operations involving dimensioned variables. The proposed method allows checking the correct use of dimensioned arguments in C++ class methods. This detection rate depends on the distribution of operations and dimensions in the C++ source files [9]. It serves as a complementary verification technique that targets defect classes often missed by conventional testing, based on the intrinsic characteristics of the software. Additionally, the method has the potential for continuous improvement, offering opportunities to further increase detection rates and overall reliability.
Together, these benefits underscore the method’s effectiveness as a practical tool for software defect detection. Its high detection rate, along with reduced testing efforts and improved reliability, make it a compelling addition to the suite of formal verification techniques. The implementation of the proposed method using metaprogramming increases the reliability of software code, as the C/C++ compiler can perform formal verification at compile time [16].
However, the method does have certain limitations. Chief among them is the requirement for explicit knowledge of the physical dimensions and orientations of source variables at compile-time. Despite this constraint, the method enhances programmer productivity by automating the detection of dimensional and orientational inconsistencies. It also enables comprehensive dimensional correctness checks across variables, operations, functions, and procedures through argument verification.
While the method shows considerable promise in improving software reliability, its full potential in complex software systems will only be realized through further research and the development of specialized analysis tools.
We are grateful to Dr. D.I. Chumachenko for the invitation to participate in the conference, as well as to our colleagues from National Aerospace University for their support and assistance.
During the preparation of this work, the authors used GPT-5 and Grammarly in order to: grammar and spelling check. After using these tools the authors reviewed and edited the content as needed and takes full responsibility for the publication’s content. [9] Manzhos, Y.; Sokolova, Y. A Software Verification Method for the Internet of Things and
Cyber-Physical Systems. Computation (2023), 11, 135. doi: 10.3390/computation11070135.
[10] Manzhos, Y.; Sokolova, Y. A type system for formal verification of cyber-physical systems
C/C++ software. Radioelectronic and Computer Systems (2024), 1: 127-142.
doi:10.32620/reks.2024.1.11.
[11] Martínez-Rojas, J.A.; Fernández-Sánchez, J.L. Combining dimensional analysis with model
based systems engineering. Syst. Eng. (2022), 26: 71–87. doi:10.1002/sys.21646.
[12] Glavič P. Review of the International Systems of Quantities and Units Usage. Standards. (2021)
1(