Formally and Empirically Verified Methodologies for Scalable Hierarchical Full-Stack Systems

Type of the Paper (Article) Formally and Empirically Verified Methodologies for Scalable Hierarchical Full-Stack Systems Dong Liu 1* 1 IBM Consulting; [email protected] * Correspondence: [email protected] Abstract This paper introduces Primary Breadth-First Development (PBFD) and Primary DepthFirst Development (PDFD)—formally and empirically verified methodologies for scalable, industrial-grade full-stack software engineering. Both approaches enforce structural and behavioral correctness through graph-theoretic modeling, bridging formal methods and real-world practice. PBFD and PDFD model software development as layered directed graphs with unified state machines, verified using Communicating Sequential Processes (CSP) and Linear Temporal Logic (LTL). This guarantees bounded-refinement termination, deadlock freedom, and structural completeness. To manage hierarchical data at scale, we present the Three-Level Encapsulation (TLE)—a novel bitmask-based encoding scheme. TLE operations are verified via CSP failures-divergences refinement, ensuring constant-time updates and compact storage that underpin PBFD's robust performance. PBFD demonstrates exceptional industrial viability through eight years of enterprise deployment with zero critical failures, achieving approximately 20× faster development than Salesforce OmniScript, 7–8× faster query performance, and 11.7× storage reduction compared to conventional relational models. These results are established through longitudinal observational studies, quasi-experimental runtime comparisons, and controlled schema-level experiments. Open-source Minimum Viable Product implementations validate key behavioral properties, including bounded refinement and constant-time bitmask operations, under reproducible conditions. All implementations, formal specifications, and non-proprietary datasets are publicly available. Keywords: Formal verification; Full-stack development; Graph-based software engineering; Hierarchical data systems; Bitmask encoding; Communicating Sequential Processes; Linear Temporal Logic; Empirical software engineering; Industrial validation 1. Introduction 1.1. Background Modern Full-Stack Software Development (FSSD) integrates frontend interfaces, backend services, data models, and deployment tooling into cohesive, multi-tier applications. Popular stacks—such as MEAN, MERN, LAMP, and Spring Boot— provide standardized frameworks to support this integration across layers. The demand for full-stack developers has surged due to their ability to manage end-to-end development, a trend consistently reflected in workforce projections and training curricula [1-5]. 2 of 186 Professional programs like IBM’s Full Stack Developer Certificate now emphasize cloud-native architecture, AI integration, and DevOps practices [3], trends aligned with the broader shift toward scalable, AI-augmented full-stack workflows [1-2]. In practice, FSSD projects typically adopt a backend-first sequence, beginning with data modeling, API design, and business logic before frontend integration. This ordering aligns with Agile principles, which emphasize incremental delivery, stakeholder feedback, and adaptability [6]. Yet despite their flexibility, Agile approaches lack formal mechanisms for dependency modeling or correctness enforcement across layers [7–8]. Stojanovic et al. [9] and Mognon and Stadzisz [10] observe that the de-emphasis on architectural specification in Agile environments introduces coordination overhead and increases integration risk in complex systems. Existing literature on FSSD focuses largely on imperative workflows and technology stacks [11-12], with limited use of formal abstractions such as graph traversal, finite automata, or process algebra. The absence of mathematically grounded models hinders scalability, maintainability, and correctness in deeply interdependent systems. Without a unifying theoretical foundation, developers lack principled tools to reason about dependencies, enforce consistency, or optimize control flow across layers [13-14]. This need for rigor is echoed in recent work on orchestration and agent-based coordination, which has reinforced the importance of verifiable models in enterprise-scale environments [15]. These findings highlight the limitations of ad hoc sequencing and motivate the integration of formal semantics into full-stack workflows. To address this gap, this paper introduces two methodologies—Primary BreadthFirst Development (PBFD) and Primary Depth-First Development (PDFD)—that reframe FSSD as a formally verifiable workflow problem, expanding on a framework initially proposed in [16][17]. Grounded in graph theory, state machines, process algebra, and Linear Temporal Logic (LTL), PBFD and PDFD integrate with Agile practices while adding precision, scalability, and correctness guarantees. Although developed for FSSD, the models generalize to broader classes of hierarchical and dependency-aware systems (see Section 3). 1.2. Motivation Enterprise-scale full-stack systems face escalating complexity, particularly in coordinating frontend, backend, and data layers. In the absence of formally specified workflows, development teams often rely on informal, tool-driven processes that suffice for small applications but break down under scale. This leads to fragmented dependencies, inconsistent state propagation, and growing technical debt—a well-documented challenge that affects both organizational outcomes and developer satisfaction [18-19]. Fragmented Dependency and Coordination Bottlenecks Disconnected workflows across layers result in duplicated validation logic and unpredictable system behavior. Kretschmer et al. [20] show that inconsistent state propagation arises when changes in one part of a system fail to trigger coordinated updates elsewhere, leading to architectural drift and regression. Tkalich et al. [21] attribute frequent integration breakdowns in large-scale continuous engineering environments to the absence of formal dependency modeling. This problem is exemplified by one of our large claims processing platforms, where weak coordination between front-end states and backend APIs triggered cascading failures, requiring weeks of remediation. Technical Debt and Productivity Loss Ad hoc implementation choices accumulate as technical debt in the absence of formal validation. Besker et al. [18] report that developers spend over 20% of their time addressing debt-related inefficiencies. Perera et al. [19] provide a systematic mapping of technical debt quantification approaches, revealing gaps in remediation strategies and highlighting 3 of 186 the organizational cost of unmanaged debt. Behutiye et al. [22] further show that reduced productivity, system degradation, and increased maintenance cost are among the most significant consequences of technical debt in Agile environments. The same system we developed accumulated over 2,000 unresolved tickets due to ad hoc coordination, delaying milestones and increasing cost. Performance and Scalability Constraints Legacy schema designs often prioritize readability or normalization over computational efficiency, leading to significant performance bottlenecks and storage overhead in enterprise-scale full-stack systems. Arulraj et al. [23] demonstrate that hybrid transactional and analytical workloads—common in full-stack architectures—suffer from high latency and poor throughput in traditional row-store schemas, highlighting a fundamental limitation of schema-first design without formal orchestration. In one of our enterprisescale systems, relational schemas consumed 11.7× more storage and exhibited O(n) query latency—causing responsiveness issues during peak operations (see Appendix 22 for a detailed case study). Cognitive Overhead and Developer Friction Repeated transitions between backend schema updates and frontend logic introduce cognitive load and procedural friction. Meyer et al. [24] show that frequent context switching reduces developer productivity and erodes motivation, especially in systems lacking structural coherence. Etikyala and Etikyala [25] demonstrate how orchestrators such as Apache Airflow and Temporal reduce developer burden by managing dependencies and improving fault tolerance. Nevertheless, in the absence of such formalisms at the development workflow level, one of our mission-critical deliveries suffered from repeated context shifts that hindered team velocity and introduced regression defects, despite an experienced team. To address these systemic limitations in dependency management, technical debt, performance, and cognitive overhead, we developed Primary Breadth-First Development (PBFD) and Primary Depth-First Development (PDFD). Building on prior exploratory work [16][17], the models presented in this paper aim to replace ad hoc sequencing and dependency management with principled, automation-ready solutions. 1.3. Contributions This paper introduces a unified formal and practical framework that advances the rigor, scalability, and verifiability of full-stack software development through four primary contributions: 1. Graph-Theoretic Formal Verified Development Framework We formalize software development as graph traversal over layered directed acyclic graphs, represented with unified state machines and verified using Communicating Sequential Processes (CSP) and Linear Temporal Logic (LTL). Four foundational models (Directed Acyclic Development, Depth-First Development, Breadth-First Development, Cyclic Directed Development) are synthesized into two hybrid methodologies—Primary Breadth-First Development (PBFD) and Primary Depth-First Development (PDFD)—with provable properties including termination, deadlock freedom, dependency preservation, and finalization invariance. 2. Three-Level Encapsulation for Hierarchical Data We introduce Three-Level Encapsulation (TLE), a bitmask-based encoding pattern achieving O(1) hierarchical operations with 11.7x storage reduction and 85.7x smaller indexes compared to normalized relational schemas. TLE's correctness is established through CSP trace refinement and formal complexity proofs (Theorems A.10.1– A.10.4), enabling predictable, high-performance hierarchical data handling. 4 of 186 3. Machine-Checked Formal Verification All workflow semantics (DAD, DFD, BFD, CDD, PBFD, PDFD) and data operations (TLE: LOAD, READ, WRITE, COMMIT) are machine-checked using FDR4 refinement checker [26,27], establishing deadlock freedom, liveness, bounded refinement, and failures-divergences correctness. 4. Rigorous Industrial Validation Eight-year enterprise deployment with zero critical failures demonstrates 20x faster development cycles, 7–8x faster queries, and 11.7x storage reduction. Results are established through longitudinal observational studies (Appendix A.20), quasi-experimental runtime comparisons (Appendix A.21), and controlled schema experiments (Appendix A.22). Open-source MVPs [28–30] ensure reproducibility. Scholarly Impact: Existing approaches—including agile feature delivery, low-code platforms, and normalized database schemas—lack formal guarantees for hierarchical systems. PDFD and PBFD establish the first graph-theoretic, formally verified foundation for full-stack development, uniting mathematical rigor with demonstrated industrial scalability. 2. Related Work This section situates our work within the broader landscape of software engineering research, focusing on four interrelated research streams: (1) domain-driven and collaborative design, (2) formal development methods such as CSP and LTL, (3) state-based traversal and process-oriented methodologies, and (4) hierarchical data structures with encoded representations. We analyze the limitations of existing paradigms and highlight how Primary Breadth-First Development (PBFD), augmented by Three-Level Encapsulation (TLE), and Primary Depth-First Development (PDFD) integrate and extend these foundations to address a persistent gap in scalable, verifiable full-stack software engineering. 2.1. Domain-Driven Design, Collaborative Modeling, and Low-Code Platforms Domain-Driven Design (DDD) has significantly influenced software engineering by emphasizing alignment between software architecture and business domains through constructs like bounded contexts and ubiquitous language [31]. Collaborative practices such as EventStorming [32] extend this further by facilitating stakeholder workshops to build shared understanding. However, these approaches remain fundamentally heuristic: they lack executable semantics, formal operational guidance, and mechanisms to ensure consistency or correctness in the resulting models [33]. This often leads to ambiguity and significant challenges in scaling collaborative models to complex, hierarchical enterprise systems. These limitations have contributed to the growing appeal of Low-Code Development Platforms (LCDPs) (e.g., Mendix, OutSystems, Microsoft Power Apps), which promise to accelerate development through visual modeling and automation [34]. While LCDPs operationalize domain concepts, they often do so with opaque orchestration logic, limited extensibility, and no formal guarantees of correctness [35]. They prioritize speed over verifiability, making them unsuitable for high-assurance systems. PBFD and PDFD address these limitations by transforming collaborative modeling into a disciplined, verifiable process. Unlike DDD’s reliance on emergent consensus or LCDPs’ black-box automation, our methodologies provide algorithmically defined traversal strategies that enforce a rigorous sequence of development. For instance, PBFD’s level-wise progression ensures domain patterns are finalized in an order that aligns with both stakeholder accessibility and architectural dependencies, while PDFD’s depth-first 5 of 186 refinement guarantees detailed feature completion before horizontal expansion. By embedding formal guarantees of termination, consistency, and correctness directly into the modeling lifecycle, PBFD and PDFD bridge the critical gap between collaborative design and a transparent, executable implementation. 2.2. Formal Methods, LTL, and Model-Driven Engineering Formal methods, including algebraic specification [36], Z [37], and Alloy [38], provide rigorous frameworks for specifying and verifying software systems. These approaches offer strong guarantees of soundness and precision but are often criticized for their steep learning curves and limited integration into practical, iterative development workflows [39]. Recent editorial perspectives emphasize that formal methods must be grounded in concrete modeling challenges to achieve broader impact in software and systems engineering [40]. Model-Driven Engineering (MDE) emerged to bridge this gap by elevating models to primary artifacts and automating implementation through model transformations [41]. However, MDE frequently struggles with aligning high-level models to evolving requirements, maintaining practicality in large-scale applications, and overcoming the "modeling bottleneck" [42,43]. Many MDE initiatives have failed to transition from academic research to widespread industrial adoption due to this complexity [44]. PBFD and PDFD integrate formal rigor directly into the development process without requiring practitioners to adopt entirely new specification languages or complex transformation frameworks. Our methodologies incorporate well-founded relations, inductive invariants, and process-algebraic semantics (e.g., CSP [45]) into the traversal logic itself. Additionally, Linear Temporal Logic (LTL) is a cornerstone of model checking [46], providing a formal language to specify and verify temporal properties such as liveness, safety, and eventual completion. While traditional approaches apply CSP and LTL for system analysis, PBFD and PDFD elevate them to primary methods for governing the development process itself, enabling correctness verification as an inherent property of development workflows. This integration lowers the adoption barrier by embedding verification into the operational semantics of development, rather than as a separate post-hoc phase. Consequently, PBFD and PDFD extend the MDE vision by offering formal correctness guarantees through pragmatic traversal strategies accessible to developers familiar with modern agile practices. 2.3. State-Based and Traversal-Oriented Approaches State machines [47], Petri nets [48], and process algebras like CSP [45] provide foundational models for reasoning about concurrency, sequencing, and state transitions. These frameworks have profoundly influenced areas like verification, scheduling, and dependency analysis. More recently, traversal-based algorithms (e.g., BFS, DFS) have been incorporated into model checking [46] and dependency-aware development tools [49,50]. However, in existing work, these techniques are typically applied as auxiliary mechanisms for analysis rather than as primary, governing principles for structuring the entire development process. A key limitation is the general absence of built-in support for safe rollback and state recovery, which is crucial for managing iterative refinement in complex projects. PBFD and PDFD advance this field by elevating traversal strategies to first-class citizens in software development methodology. Unlike traditional uses of BFS/DFS as support functions, our methodologies encode traversal logic directly into the state machine and process algebra that govern development progression. This allows properties like correctness, termination, and rollback safety to be derived directly from the traversal semantics. Beyond correctness, our approach supports rollback safety and iterative refinement— 6 of 186 features often missing in traditional state-based models. By doing so, PBFD and PDFD establish a formal and practical bridge between classical state-based reasoning and the complexities of modern full-stack development, enabling a new paradigm of verifiable and scalable software construction. 2.4. Encoded Data Structures and Hierarchical Storage Efficiently managing hierarchical data in relational systems has long been a challenge, typically relying on recursive mechanisms (e.g., Recursive CTEs on adjacency lists) that yield complexity proportional to the depth or size of the hierarchy, incurring substantial O(log n) lookup costs and high query overhead [51,52]. This complexity directly contributes to the performance and scalability issues discussed in Section 1.2. Our work is related to research in high-performance encoded data systems. Database designs like column-stores prioritize encoding and compression techniques to achieve faster query processing and reduced I/O [53 - 55]. The use of bitwise operations for fast filtering and lookup is a well-established principle in this domain. However, this work focuses on internal query optimization within the DBMS, whereas our Three-Level Encapsulation (TLE) model introduces a declarative bitmask-based schema pattern, a technique that uses bitwise operations to store and manipulate multiple Boolean states within a single integer field, externalizing optimization to the application layer. In contrast, the TLE model enables O(1) lookup, update, and traversal while remaining fully compatible with standard relational platforms. By formalizing hierarchical semantics through bitmask encoding rather than traditional approaches like adjacency lists or nested sets, TLE bridges the gap between encoded data representations and application-level correctness—offering a formally verifiable alternative to materialized path or encoded columnar models not addressed in prior hierarchical storage research. 2.5. Synthesis and Positioning of PBFD/PDFD As summarized in Table 1, existing research strands exhibit complementary strengths and limitations. DDD and collaborative modeling excel at fostering shared understanding but lack formal execution. Formal methods offer rigor but suffer from practicality issues. Traversal and state-based approaches provide analytical power but are rarely central to development methodologies. Encoded hierarchical storage approaches optimize performance but do not address formal correctness or integrated workflow management. Table 1. Positioning of PBFD and PDFD Against Existing Research Paradigms. Research Area Typical Limitations in Prior Work PBFD/PDFD Contributions Domain-Driven Design & Collaborative Modeling [31, 32] Heuristic, non-executable, lacks formal consistency guarantees Formal semantics with executable workflow rules; ensures verifiable consistency Formal Methods & LTL [39,40,44,48] High abstraction, steep learning curve, limited integration with practice Embedded rigor within accessible workflows; verification of temporal properties (liveness, safety, eventual completion) State Machines & Traversal Algorithms [47,48] Used as auxiliary tools, not primary development drivers Traversal as a first-class development primitive; enables derivation of correctness properties, rollback safety Model-Driven Engineering [41-44] Struggles with evolving requirements, scalability, and industrial adoption Pragmatic adaptability combined with formal foundation; scales to enterprise systems Low-Code Development Platforms [34, 35] Opaque orchestration, limited extensibility, correctness not guaranteed Transparent, graph-based orchestration; ensures structural correctness and extensibility 7 of 186 Research Area Typical Limitations in Prior Work PBFD/PDFD Contributions Encoded Data Structures, Columnar Encoding, Bitmap Indexes [52,54,55] Encoding used internally by DBMS for query acceleration; hierarchical relations still require recursive/nested traversal (O(log n)); no formal semantics for hierarchy or correctness Declarative bitmask-based hierarchical schema (TLE); O(1) lookup/update/traversal; externalizes encoding at schema design level; preserves explicit hierarchical semantics and enables formal verification (CSP/LTL) PBFD and PDFD synthesize these domains into a unified framework. Our methodologies leverage graph-based traversal as the core organizing principle for development, ensuring structured progression, formal verifiability, and practical adaptability. This integration addresses a persistent gap in the literature: the lack of a scalable, verifiable methodology that spans from collaborative design to full-stack implementation, while maintaining the rigor demanded by high-assurance systems (see Table 1). Together, PBFD and PDFD provide a coherent foundation for automating, verifying, and scaling hierarchical full-stack systems, directly addressing the tensions between flexibility, rigor, and practicality that have long challenged the software engineering community. 3. Formal Framework and Methodologies 3.1. Introduction and Motivation While Section 1 establishes the practical challenges of full-stack development, this section introduces a unified formal framework for reasoning about and comparing the software development methodologies that address them. Prior research has employed distinct formalisms—Petri nets for state modeling [56], process calculi for communication semantics [57], and temporal logic for property specification [46]—yet these techniques often operate in isolation, lacking systematic integration for cross-paradigm comparative analysis. This fragmentation persists despite calls for formal methods to engage with concrete modeling challenges to achieve lasting impact in software and systems engineering [40]. Our framework addresses this gap by formalizing development workflows as directed dependency graphs with traversal-driven development semantics. A software system under development is represented as a directed graph G = (V, E), where vertices V denote Structural Entities—the units of development, refinement, or verification (e.g., modules, components, features, data schemas, or architectural layers)—and edges E ⊆ V × V capture precedence constraints, semantic dependencies, or compositional relationships. Development follows systematic traversal of this graph, implementing either Primary Breadth-First Development (PBFD) where nodes typically represent pattern instances, or Primary Depth-First Development (PDFD, where nodes may correspond to business data elements—such as countries, states, or schemas—depending on project constraints. Methodologies are defined as systematic traversal strategies over this graph, governed by state machines that specify control flow, vertex selection rules, and refinement logic. This abstraction enables rigorous reasoning about critical correctness properties, including: • Termination — The development process completes in finite time, visiting all reachable vertices. • Deadlock freedom — No circular dependency chains prevent progress (i.e., the graph is acyclic or cycles are explicitly managed). • Dependency satisfaction— All prerequisite vertices are processed before their dependents, respecting the partial order imposed by E. • Completeness—All vertices representing required system components are eventually processed and verified. 8 of 186 To ensure rigor and verifiability [58][59], the framework integrates multiple complementary representational layers: • Structural diagrams visualize workflow architecture and traversal paths. • State machines define precise operational semantics and control logic. • Unified transition tables specify deterministic rules linking states, conditions, and actions. • Pseudocode encodes algorithmic logic for traversal, validation, and refinement. • Communicating Sequential Processes (CSP) [45] model concurrent execution and inter-process communication, with execution traces serving as the semantic basis for temporal verification. • Linear Temporal Logic (LTL) [60] specifies global temporal properties—such as liveness, termination, and rollback safety—to be proven over all possible CSP traces. This hybrid approach supports both local reasoning (via state machines) and global verification (via CSP and LTL). Verification combines automated, instance-based model checking with generalizable correctness proofs derived from transition rules and graphtheoretic invariants. By embedding verification directly into workflow semantics, the framework transforms the design of methodologies such as PBFD and PDFD from a largely heuristic practice into a formally grounded, reproducible engineering discipline [61]. 3.2. Formal Notation and Communication Conventions To support reproducibility and cross-methodology comparison, we standardize notation and communication across all representational layers. Formal definitions for logic symbols, state identifiers, and transition semantics are provided in Appendix A.1. Each methodology is expressed through the following integrated representations: • Pseudocode: Defined as Procedure [Name](...) with explicit inputs, outputs, and traversal logic. • CSP Specifications: All formal models use synchronous channels to represent communication and control flow. Each specification is validated in FDR 4.2.7, with complete source code and verification scripts available in the corresponding appendices A.2–A.7 and linked GitHub repositories. • Unified Transition Tables: Specify formal transition rules between states, including conditions, actions, and branching logic. • Structural Diagrams: Mermaid-based diagrams visualize workflow structure and state transitions. Source code is provided in the respective appendices. • Cross-Representational Mappings: Appendices A.2–A.7 include full mappings between pseudocode, CSP specifications, and transition tables, ensuring consistency and enable reproducibility across diverse implementation contexts. The LTL properties defined for each methodology (e.g., termination, liveness, and dependency completeness) are evaluated over the observable traces of their verified CSP processes. For basic methodologies, representative properties are verified; for hybrid methodologies (PBFD and PDFD), all key temporal properties are formally proven in Appendix A.8. These properties are derived from each methodology’s transition rules and foundational graph algorithms [62, 63]. This layered formalism ensures that each methodology is both executable and verifiable across structural, operational, and temporal dimensions, providing a rigorous foundation for comparative reasoning and scalable adoption. 3.3. Basic Methodologies The basic methodologies are rigorous graph-theoretic abstractions, each derived from a fundamental traversal or dependency structure. Rather than prescriptive software 9 of 186 engineering practices, they serve as composable formal models that capture distinct workflow strategies: • Directed Acyclic Development (DAD): Enforces strict, non-cyclic dependencies to ensure monotonic progress and traceability. Its full formal specification is provided in Appendix A.2. • Depth-First Development (DFD): Derived from depth-first search (DFS). Prioritizes vertical exploration by completing deep dependency chains before addressing sibling units. Its full formal specification is provided in Appendix A.3. • Breadth-First Development (BFD): Derived from breadth-first search (BFS). Promotes horizontal, level-wise traversal to maintain cross-component consistency at each stage. Its full formal specification is provided in Appendix A.4. • Cyclic Directed Development (CDD): Based on cyclic directed graphs. Incorporates bounded feedback loops within otherwise acyclic workflows, supporting structured reprocessing for iterative refinement. Its full formal specification is provided in Appendix A.5. Together, these methodologies establish the foundational traversal patterns and dependency constraints upon which hybrid approaches, such as PDFD and PBFD, are later defined. 3.3.1. Directed Acyclic Development (DAD) Directed Acyclic Development (DAD) is a hierarchical, dependency-driven methodology that organizes software construction around a strict-dependency chain. It ensures that a given node can only be processed once all of its direct dependencies (D(v)) have been completed and validated. This approach guarantees logical correctness by enforcing that all foundational components are finalized before any dependent features are developed. The core of this methodology is derived from graph-based dependency analysis and a topological sort algorithm, ensuring a valid and predictable order of execution. 1. Definition and Formalization Definition: Directed Acyclic Development (DAD) structures development as a DAG G = (V, E), where: • Nodes represent components (e.g., modules, tasks). • Edges represent irreversible dependencies ((u, v) means u must complete before v). • Acyclicity ensures no cycles exist, preventing deadlocks or circular dependencies. Formal Parameters: The structural elements of DAD are defined in Table 2. Table 2. Formal parameters for the DAD model. Symbol Description G Directed Acyclic Graph with vertices V and edges E D(v) Direct dependencies of node v: {u|(u, v) ∈ E} 2. Key Characteristics The essential features of DAD are summarized in Table 3. Table 3. Key characteristics of DAD. Characteristic Description Acyclic Enforcement Ensures that the development dependency graph remains acyclic, preventing circular dependencies and infinite traversal loops Scalability Supports incremental addition of nodes and edges, provided that the overall graph preserves its acyclic structure 16 of 186 This section confirms that the CSPM model (See Appendix 3.4) of the DFD pipeline satisfies the formal properties verified using the FDR model checker. The verification demonstrates that the concrete DFD implementation adheres to behavioral constraints, stack-based traversal, and liveness requirements expressed in the DFD specification. The results below show that DFD’s depth-first traversal mechanism—specifically its pre-order node handling, child stack management, and ordered completion—is formally correct (see Table 13). Table 13. Summary of verification results. Property CSP Assertion FDR Result Engineering Significance Core Safety DFD :[deadlock free [F]] ✓ Passed Ensures no blocking states occur during subtree processing or backtracking Core Liveness DFD :[divergence free] ✓ Passed Confirms absence of τ-cycles or infinite descent during traversal Determinism DFD :[deterministic [F]] ✓ Passed Guarantees predictable recursion and unambiguous subtree completion Local Processing Safety DequeueThenProcess [T= DFD_Core] ✓ Passed Ensures each dequeued node is immediately processed (DF2 & DF3) Non-Leaf Descent Logic NonLeafPushesChildren [T= DFD_Core] ✓ Passed Enforces DF2: non-leaf nodes must push their children before continuing descent Leaf/Backtrack Initiation LeafToBacktrack [T= DFD_Core] ✓ Passed Enforces DF3: processing a leaf correctly triggers parentlevel backtracking Validation Control Flow ValidationSequence [T= DFD_Core] ✓ Passed Ensures validation transitions lead only to backtracking or termination (DF5–DF7) Termination Reachability TerminationAllowed [T= DFD_Core] ✓ Passed Confirms the system can always reach the final successful state Interpretation & Contributions Depth-first execution guarantees Assertions DequeueThenProcess, NonLeafPushesChildren, and LeafToBacktrack formally verify DFD’s pre-order, stack-based traversal: • Nodes are processed as soon as they are dequeued (DF2–DF3). • Non-leaf nodes correctly push their children before descent. • Leaf processing reliably initiates the backtracking sequence. These behaviors confirm correctness of the S1 (Vertical Processing) state and DF2/DF3 rules. Subtree completion and termination guarantees Assertions ValidationSequence and TerminationAllowed verify: • The system cannot stall in backtracking or validation cycles (DF5–DF7). • All hierarchical paths are completed before termination. • Final termination is guaranteed once traversal is exhausted. Together, these ensure proper state flow through S2/S3 and eventual termination. Practical significance Collectively, the results show that DFD: • Supports correct recursive descent through hierarchical structures using deterministic stack operations • Ensures subtree completion before parent-level progression • Avoids deadlocks, livelocks, and nondeterministic backtracking 8. LTL Properties To ensure correctness and termination of the DFD workflow, we define its global properties using Linear Temporal Logic (LTL), as shown in Table 14. 17 of 186 Table 14. LTL properties of DFD ensuring correctness and termination. Property Formal Specification Description Single Path Completion □∀P = (C₀, ..., Cᴸ) ∈ G: (processed(Cᴸ) ⇒ ∀Cⱼ ∈ P, processed(Cⱼ)) A path is processed completely before moving to siblings (Rules DF2, DF3). Subtree Validation Completeness □(validated(Bⱼ) ⇒ ∀Cₖ ∈ Subtree(Bⱼ), validated(Cₖ)) A subtree is only validated after all nodes within it are processed (Rules DF5, DF6). Liveness (No Starvation) ∀ v ∈ V, ♢processed(v) Every node is eventually processed (Rules DF4, DF6). Termination Guarantee □(start(DFD) ⇒ ◊terminate(DFD)) The process eventually terminates for any finite tree (Rule DF7). 9. Advantages The benefits of applying DFD are summarized in Table 15. Table 8. Advantages of DFD in dependency-aware systems. Property Advantage Early Validation Foundational logic (e.g., country → state → city) is validated early. Modular Testing Bugs are isolated within narrow vertical paths. Incremental Scaling New nodes or branches can be integrated without restructuring validated paths. The full formal specification for DFD is provided in Appendix A.3. 3.3.3. Breadth-First Development (BFD) Breadth-First Development (BFD) organizes software construction around horizontal progression across architectural levels. The methodology ensures that all nodes at a given depth are processed and validated before advancing to subsequent levels, thereby enforcing layered correctness and predictable advancement. This approach is conceptually derived from the Breadth-First Search (BFS) graph traversal algorithm [63, 64]. 1. Definition and Formalization Definition: Breadth-First Development (BFD) is a hierarchical methodology that processes all nodes at level k before descending to level k+1. This guarantees uniform development across parallel branches of the system and enforces synchronization within each architectural layer, a strategy that aligns with architectural design principles [65]. Node Semantics: Each Nₖ represents a set of semantic units (e.g., modules, tasks, or components) located at architectural depth k in the dependency graph. Formal Parameters: The structural elements of BFD are summarized in Table 16. In this model, edges are directional, with v→u indicating that node v must be completed before node u can begin. Here, D(v) refers to the set of direct successors (children) of v. Table 16. Formal parameters for the BFD model Symbol Description Q Global queue tracking nodes to process Nₖ Set of nodes at level k L Maximum depth level of the tree D(v) Set of direct successors to node v, i.e., {u∣(v,u)∈E} 2. Key Characteristics The structural and operational characteristics of BFD are listed in Table 17. Table 17. Key characteristics of BFD. Characteristic Description Horizontal Progression All nodes at a given level must be processed before the algorithm proceeds to the next level. 18 of 186 Characteristic Description Layered Advancement Advancement from level k to k+1 occurs only after all nodes at level k are processed and validated. Level Synchronization Maintains level integrity, ensuring consistency across parallel node implementations within the same level. 3. Workflow Representation Figure 6 shows the conceptual flow of an eight-node, three-level BFD model, emphasizing horizontal traversal at each level. The MermaidJS source code is provided in Appendix A.4.1. Figure 6. Structural workflow of BFD illustrating horizontal processing across each level 4. State Descriptions The states of the BFD process model are defined in Table 18. Table 18. State definitions in the BFD process model. State ID Phase Description S₀ Initialization Load graph and initialize level queues S₁ Level Processing Process nodes at level k S₂ Validation Validate all nodes at level k T Termination Final state after all levels are completed 5. Unified State Transition Table The formal transition rules governing the BFD workflow are defined in Table 19. Table 19. Formal state transitions and workflow operations in BFD. Rule ID Source State Target State Condition Operational Step BF1 S₀ S₁ Graph loaded. Initialize queue Q with root BF2 S₁ S₁ Q≠∅∧(∃c∈Nₖ:¬processed(c)) Process next node in current level BF3 S₁ S₂ ∀c∈ Nₖ:processed(c) Validate level k BF4 S₂ S₁ k<L Advance to level k+1 BF5 S₂ T k=L Terminate 6. State Machine Diagram Figure 7 depicts the BFD state machine model, corresponding to the transitions in Table 19. The corresponding MermaidJS source code is available in Appendix A.4.2. 7. CSP Formal Verification Results and Guarantees for BFD This section confirms that the CSPM model (see Appendix A.4.4) of the BFD pipeline satisfies the formal properties verified using the FDR model checker. The verification demonstrates that the concrete BFD implementation adheres to behavioral constraints, liveness requirements, and robustness goals expressed in the BFD specification. The results below demonstrate that BFD’s breadth-first traversal mechanism—particularly its safe handling of level queues, node processing, and level validation—is formally correct (see Table 20). 19 of 186 Figure 7. State machine model of BFD showing transitions BF1–BF5. Table 20. Summary of verification results. Property CSP Assertion FDR Result Engineering Significance Core Safety BFD :[deadlock free [F]] ✓ Passed Guarantees liveness across node and level processing (no terminal blocking states) Core Liveness BFD :[divergence free] ✓ Passed Confirms absence of livelock and infinite internal loops (τ-cycles) Determinism BFD :[deterministic [F]] ✓ Passed Ensures that queue and node processing decisions are uniquely defined for predictable execution Safety: Dequeue Implies Process DequeueImpliesProcess [T= BFD_Core] ✓ Passed Confirms that each dequeued node is immediately processed, preserving workflow correctness (BF2) Level Validation Before Advancement ValidateBeforeAdvance [T= BFD_Core] ✓ Passed Ensures that all nodes at level k are validated before moving to level k+1 (BF3 & BF4) Post-Validation Behavior AfterValidation [T= BFD_Core] ✓ Passed Guarantees that after level validation, the process either advances or terminates (BF4 & BF5), ensuring progress. Successful Termination terminate_successfully_actual -> SKIP [T= CanReachTerminate] ✓ Passed Demonstrates that BFD completes all levels and nodes successfully (BF5) Termination at End TerminationAtEnd [T= BFD_Core] ✓ Passed Confirms that termination occurs only after all processing and validation steps are complete Interpretation & Contributions Breadth-first execution guarantees Assertions DequeueImpliesProcess and ValidateBeforeAdvance formally verify BFD’s breadth-first execution semantics: • Each node in the current level queue is dequeued and processed before moving to the next node. • Level advancement occurs only after all nodes in the current level are validated. Together, these ensure that breadth-first traversal respects hierarchical dependencies (BF1–BF4) and prevents premature progression to higher levels. Termination guarantees 20 of 186 Assertions CanReachTerminate and TerminationAtEnd confirm that: • BFD can always successfully reach the termination state terminate_successfully_actual. • All nodes and levels are fully processed, ensuring liveness and preventing livelock (BF5). Practical significance Collectively, the results show that BFD: • Supports safe, level-by-level processing of hierarchical structures • Guarantees full completion and validation of each level before moving to the next • Prevents deadlocks or livelocks while ensuring predictable, deterministic behavior • Ensures internal consistency and milestone integrity through explicit assertions on processing order, validation, and termination 8. LTL Properties To ensure layered correctness and termination, we define the global properties of BFD using Linear Temporal Logic (LTL), as shown in Table 21. Note that processed (Nₖ) is a shorthand for ∀c∈Nₖ:processed(c). Table 21. LTL properties of BFD ensuring layered correctness and termination. Property Formal Specification Description Layer Completion □∀k≤L: (processed(Nₖ) ⇒ ¬∃Cⱼ∈Nₖ: ¬processed(Cⱼ)) All nodes in a level are processed before proceeding (Rules BF2, BF3). Order Preservation □∀k<L: (validated(Nₖ) ⇒ ◊processed(Nₖ₊₁)) Level k+1 is entered only after all nodes at level k are validated (Rules BF3, BF4). Termination Guarantee □(start(BFD) ⇒ ◊terminate(BFD)) Process reaches completion (Rules BF4, BF5). Liveness (No Starvation) □∀v∈V, ◊processed(v) Every node in the graph is eventually processed. 9. Advantages The benefits of applying BFD are summarized in Table 22. Table 22. Advantages of BFD in dependency-aware systems. Property Advantage Consistency Uniform implementation across layers (e.g., all Level 1 nodes completed before Level 2) Parallelization Nodes at the same level can be processed concurrently Predictability Clear level-based rules simplify debugging (errors are localized to a single level) The full formal specification for BFD is provided in Appendix A.4. 3.3.4. Cyclic Directed Development (CDD) Cyclic Directed Development (CDD) is a software development methodology that incorporates controlled feedback loops into the development process. Unlike linear or strictly acyclic models, CDD enables revisiting previously developed nodes based on validation or stakeholder feedback. This capability ensures adaptability while imposing formal constraints to avoid infinite regress. CDD formalizes patterns seen in Agile workflows [66], acting as a foundational model for hybrid and iterative development methods. Its behavior is formally specified via a state machine and CSP process algebra (see Appendix A.5). 1. Definition and Formalization Definition: Cyclic Directed Development (CDD) permits iterative refinement of a development graph by enabling controlled feedback loops, subject to formal convergence guarantees. 21 of 186 Node Semantics: Each node represents a semantic unit (e.g., module, component, or feature) within a directed graph that may contain cycles, representing iterative refinement points. Formal Parameters: The key parameters of CDD are summarized in Table 23. Table 23. Formal parameters for the CDD model Symbol Description G = (V, E) Directed graph (possibly cyclic) with nodes V and edges E, representing development flow and dependencies Iₖ Incremental delivery milestone k, representing a validated subset of the system Fₖ Feedback trigger mechanism (e.g., validation failure, stakeholder input) associated with milestone k Rₘₐₓ Maximum allowed refinements per node to ensure convergence 2. Key Characteristics The fundamental characteristics of CDD are outlined in Table 24. Table 24. Key characteristics of CDD supporting iterative and incremental development Characteristic Description Controlled Feedback Loops Feedback is allowed only when externally triggered and is bounded to prevent infinite iteration. Incremental Delivery Components are delivered in validated increments to support continuous integration and testing. 3. Workflow Representation Figure 8 illustrates the CDD workflow pattern, highlighting the integration of feedback loops within the development cycle to facilitate iterative refinement. The corresponding MermaidJS source code is provided in Appendix A.5.1. Figure 8. CDD workflow model integrating feedback cycles and bounded iteration 4. State Descriptions The states of the CDD process model are defined in Table 25. Table 25. State definitions in the CDD process model. State ID Phase Description S₀ Initialization Load graph and initialize dependencies S₁ Node Processing Develop components under the current milestone S₂ Refinement Iterate based on validation failure or stakeholder feedback S₃ Validation Evaluate milestone Iₖ for completeness and correctness T Termination Final increment successfully validated and delivered 5. Unified State Transition Table 22 of 186 The transitions between different states in the CDD process are captured in Table 26. Function definitions and descriptions can be found in Tables A.1.5 and A.5.1. Table 26. Formal state transitions and workflow operations in CDD. Rule ID Source State Target State Condition Operational Step CD1 S₀ S₁ Graph loaded Initialize development graph CD2 S₁ S₁ Node processed Continue node development CD3a S₁ S₂ test_failed(Cᵢ) Rework after failure CD3b S₁ S₂ feedback_triggered(Cᵢ) Apply bounded feedback loop CD4a S₂ S₁ refinement_complete(Cᵢ) Resume development on node CD4b S₂ T refinement_failed(Cᵢ) ∨ refinement_count(Cᵢ) ≥ Rₘₐₓ Terminate with error CD5 S₁ S₃ all_components_written(Iₖ) Validate increment CD6 S₃ S₂ feedback_received(Iₖ) ∨ validation_failed(Iₖ) Revision required CD7 S₃ T all_increments_validated Finalize delivery CD8 S₃ S₁ validation_successful(Iₖ) ∧ (k < L) Advance to milestone Iₖ₊₁ 6. State Machine Diagram The state machine for CDD, illustrating the cyclic transitions for refinement and validation, is depicted in Figure 9. The corresponding MermaidJS source code is available in Appendix A.5.2. Figure 9. State machine diagram of CDD showing cyclic transitions and bounded iteration. 7. CSP Formal Verification Results and Refinement Guarantees for CDD This section confirms that the CSPM model (see Appendix A.5.4) of the CDD pipeline satisfies the formal properties verified using the FDR model checker. The verification demonstrates that the concrete implementation adheres to the behavioral constraints, liveness requirements, and robustness goals expressed in the CDD specification. 23 of 186 The results below demonstrate that CDD’s enhanced architecture—particularly its safe handling of concurrent component dependencies and its guarantee of bounded, terminating refinement cycles—is formally correct (see Table 27). Table 27. Summary of verification results. Property CSP Assertion FDR Result Engineering Significance Core Safety CDD :[deadlock free] ✓ Passed Guarantees liveness throughout the deployment lifecycle (no terminal blocking states) Core Liveness CDD :[divergence free] ✓ Passed Confirms absence of livelock and infinite internal loops. Protocol Compliance (Trace) ProtocolChecker [T= CDDProtocolView] ✓ Passed Observable deployment traces conform to the defined protocol Protocol Compliance (Liveness) CDDProtocolView :[divergence free] ✓ Passed Livelock-free protocol abstraction Safety: Initial Guard NoEarlyTermination [T= CDD] ✓ Passed Prevents termination before mandatory initialization (load_graph, initialize_dependencies) Dependency Respect (Contribution N4) DependencySpec_N4 [T= CDD] ✓ Passed Proves N4 cannot execute before both N2 and N3 complete Dependency Respect (Contribution N5) DependencySpec_N5 [T= CDD] ✓ Passed Proves N5 cannot execute before N4 completes Robustness: Bounded Refinement (Deadlock) CDD_Hostile :[deadlock free] ✓ Passed Liveness retention and error-termination reachability under adversarial failure Robustness: Bounded Refinement (Divergence) CDD_Hostile :[divergence free] ✓ Passed Shows the system does not livelock under persistent failures; termination is guaranteed Internal Consistency ConditionalConsistency [T= STOP] ✓ Passed Ensures mutually exclusive conditional events do not conflict Interpretation & Contributions Dependency-aware safety Assertions DependencySpec_N4 [T= CDD] and DependencySpec_N5 [T= CDD] formally verify CDD’s concurrency and scheduling guarantees: • N4 dependency: N4 cannot start until both N2 and N3 are complete. • N5 dependency: N5 cannot start until N4 is complete. Together, these ensure that parallel processing flexibility does not violate critical sequential dependencies. Bounding guarantee under adversary The hostile-environment check (CDD_Hostile :[...]) composes CDD with HostileEnv_Refinement, an environment that persistently supplies validation_failed_actual and refinement_failed_actual. Passing the deadlock and divergence checks confirms the model enforces the refinement bound: • After Rₘₐₓ= 3 failed refinements, the process issues the error termination event terminate_with_error_actual and does not deadlock or livelock. Practical significance Collectively, the results show that CDD: • Supports safe, concurrent processing under explicit dependencies • Provides a provable defense against infinite refinement cycles by bounding retries and enforcing termination in worst-case conditions • Ensures internal consistency and milestone completion integrity through both guards and dependency assertions 8. LTL Properties 24 of 186 The global properties of CDD, defined below using Linear Temporal Logic (LTL), ensure bounded iterative refinement and guarantee termination (see Table 28). Note that validated(Iₖ) implies that all components in Iₖ are validated, and refine(Cⱼ) denotes the act of reprocessing and revalidating the node Cⱼ. Table 28. LTL properties of CDD enabling bounded iterative refinement. Property Formal Specification Description Cycle Integrity □(processed(Cⱼ) ⇒ ◊refine(Cⱼ)) ∧ □(refinement_count(Cⱼ) ≤ Rₘₐₓ) Bounded feedback loops are permitted (CD3a/CD3b). Incremental Soundness □(◊finalize(Iₖ) ⇒ ∀C ∈ Iₖ, validated(C)) All components in a milestone must be validated before release (CD5, CD7). Bounded Refinement □∀v ∈ V: (refinement_count(v) ≤ Rₘₐₓ) The number of refinements for any node is strictly bounded by Rₘₐₓ. Termination Guarantee □(start(CDD) ⇒ ◊T) The process eventually reaches successful termination. 9. Advantages The benefits of adopting the CDD methodology are summarized in Table 29. Table 29. Advantages of CDD in dependency-aware systems. Property Advantage Adaptability Supports bounded iteration in response to validation results or stakeholder feedback Risk Reduction Enables early defect detection through milestone-based validation Agile Compliance Aligns with sprint-style incremental delivery while maintaining formal convergence guarantees The full formal specification for CDD is provided in Appendix A.5. 3.4. Hybrid Methodologies Traditional methodologies struggle to reconcile the dual imperatives of modern software development—adaptability and architectural rigor. While Waterfall provides the latter but lacks the former [67], pure Agile emphasizes the former but often lacks the latter at scale [68]. In systems with deep hierarchical dependencies, this dichotomy often leads to coordination bottlenecks and technical debt [69]. These limitations are mirrored in our basic graph-based models. While Depth-First Development (DFD), Breadth-First Development (BFD), and Cyclic Directed Development (CDD) each offer unique structural strengths, they exhibit critical weaknesses in isolation: • DFD and BFD lack mechanisms for iterative adaptability. • CDD accommodates iteration but sacrifices hierarchical scaffolding. To resolve these structural and operational trade-offs, we introduce hybrid methodologies that unify vertical depth, horizontal coordination, and structured refinement. This approach parallels hybrid models in implementation science, which blend clinical effectiveness testing with implementation strategies to accelerate real-world adoption [70]. Similarly, the methodologies proposed here instantiate a dual optimization pattern: simultaneously addressing functional correctness and process efficiency. We define two primary hybrid strategies: • Primary Depth-First Development (PDFD): An adaptive, vertical progression model optimized for recursive, dependency-heavy systems requiring early risk resolution. It integrates depth-first traversal with bounded parallelism (Kᵢ) and cyclic refinement (Rₘₐₓ) to manage local complexity while securing critical paths. • Primary Breadth-First Development (PBFD): A scalable, horizontal progression model optimized for large-scale systems where architectural stability is paramount. It utilizes pattern-driven modularity (e.g., Three-Level Encapsulation) 25 of 186 to establish architectural scaffolds before engaging in selective depth-oriented refinement. By embedding verification directly into workflow semantics, these hybrids elevate methodology design into a reproducible engineering discipline that balances vertical recursion with horizontal scalability. 3.4.1. Primary Depth-First Development (PDFD) This section introduces the Primary Depth-First Development (PDFD) methodology, which serves as the foundational control model for hierarchical system development. PDFD formalizes depth-first progression, bounded parallelism, and iterative refinement. It aligns with established software architecture paradigms [65] and supports formal verification through state-space exploration [71]. 1. Foundational Concepts and Definitions Definition PDFD operates over a hierarchical structure of L levels (L ≥ 1), where nodes at each level i are collectively denoted as level(i). Each node n maintains a processing state P(n) ∈ {0, 1, 2}, with P(n) = 2 indicating finalized status. In the reference implementation, nodes represent discrete business data entities (e.g., continent, country, state), with directed edges capturing hierarchical relationships. Core Paradigms The methodology synthesizes three core paradigms: • Depth-First Development (DFD): Enables vertical progression through the hierarchy, adapted from graph traversal theory [62] for systematic elaboration of dependencies • Breadth-First Development (BFD): Constrains parallelism via threshold parameter Kᵢ, enforcing bounded work-in-progress limits that manage cognitive load [66, 72, 73] • Cyclic Directed Development (CDD): Enables iterative, validation-driven refinement with bounded limit Rₘₐₓ, providing corrective feedback without infinite loops [74] Progression Control Progression from level i to level i+1 is permitted only after at least Kᵢ nodes at level i reach finalized state (P(n) = 2). This completion-driven constraint acts as a synchronization threshold. Unlike traditional Work-In-Progress (WIP) upper bounds, Kᵢ ensures that a meaningful batch of work is validated before the system permits vertical descent. This prevents premature context switching and maintains flow efficiency. Refinement Mechanism When validation fails at level i, the function trace_origin(i) identifies the earliest affected level Jᵢ, triggering refinement across the range [Jᵢ, i]. This mechanism allows previously finalized nodes to be revisited and reprocessed if validation errors trace to earlier stages. To ensure termination and architectural consistency, the number of refinements per level is strictly bounded by Rₘₐₓ. While node status may be temporarily reset during active refinement, the process is designed to restore finalized status upon successful re-validation. Finalization Process Upon reaching terminal or blocked paths, PDFD invokes a structured finalization mechanism. This combines bottom-up subtree verification with top-down passes to complete all unprocessed nodes, ensuring global integrity. Implementation Note 32 of 186 Property Formal Specification Description & Justification decrease in k₂ (remaining refinement attempts), ensuring lexicographic progress. Finalization Permanence ∀n∈G: □((P(n)=2 ∧ ¬∃j:(refining(j) ∧ n∈affected_nodes(j))) ⇒ ◯(P(n)=2)) Corollary A.8.3.1: A finalized node's status is permanent except when an active, guarded refinement backtrack resets it; such resets are bounded and compensated by a strict decrease in k₂ (remaining refinement attempts). Descendant Finalization Invariant ∀n: □(P(n)=2 ⇒ ∀d ∈ descendants(n) ∩ processed_subtree(n), P(d)=2) Lemma A.8.5: A node is not finalized unless all nodes in its processed subtree are also finalized. Enforced by guards in PD4a, PD6, PD7. Refinement Locality □∀i,j: ((state = S₂(i) ∧ ◯state = S₁(j)) ∨ (state = S₃(i) ∧ ◯state = S₁(j)) ∨ (state = S₄(i) ∧ ◯state = S₁(j))) ⇒ (j ≤ i ∧ j = trace_origin(i)) Lemma A.8.5: All backtracking transitions target a valid anchor level j within the current progression frontier, and j is the origin of the current trace. Progression Condition □∀i: ((S₂(i) ∧ (∑_{n ∈ level(i)} [P(n)=2] ≥ Kᵢ)) ⇒ ◯(S₁(i+1))) Rule PD2b (Table A.8.2): The system advances to the next level's Initialization phase (S₁) when enough nodes (Kᵢ) at the current level are finalized. Guarded Progression Invariant □((state = S₂(i) ∧ ∑_{n∈level(i)}[eligible(n)] ≥ Kᵢ) ⇒ ◯(S₁(i+1) ∧ selected_subtree ⊆ trace(i))) Rule PD2b (Table A.8.2): Progression to the next level is guarded by eligibility criteria and trace constraints, ensuring bounded advancement. Bottom-Up Finalization □∀i: ((S₂(i) ∧ (i = L ∨ level(i+1)=∅)) ⇒ ◯(S₃(i))) Rule PD4 (Table A.8.2): Finalization initiation is triggered upon reaching a leaf node or an empty level, ensuring the transition from progression to completion. Top-Down Finalization □∀i: ((S₄(i) ∧ (∀n ∈ level(i): P(n)=2)) ⇒ ◯S₄(i+1) ∨ ◯T ∨ ◯S₅) Rule PD6 (Table A.8.2): The top-down completion phase progresses to the next level once the current level is fully finalized (or the process terminates). Global Consistency □(T ⇒ (∀n ∈ G, P(n)=2)) Rule PD7 (Table A.8.2): Successful termination implies all nodes in the graph are finalized. Vertical Closure (Forward Guarantee) □((P(n)=2 ∧ children(n) ≠ ∅) ⇒ ◊∀d ∈ children(n): P(d) ∈ {1,2} ∨ T ∨ S₅) Implied by PD4/PD6 (Table A.8.2): If a parent is finalized, its children are guaranteed to be addressed in the process flow (either by forward progression or completion), barring system termination. Soundness T ⇒ (∀n∈G: consistent(n) ∧ dependencies_satisfied(n)) Theorem A.8.8: Successful termination implies all nodes are internally consistent and satisfy their architectural dependencies, ensuring the final system is semantically correct. Unified Progress □((¬T ∧ ¬S₅) ⇒ ∃enabled_transition) Lemma A.8.7: From any non-terminal state, at least one transition rule is enabled, ensuring the system never deadlocks. Liveness (Progress) □((¬T ∧ ¬S₅) ⇒ ◯(M <_{lex} M)) Lemma A.8.7: From any non-terminal state, an enabled transition exists, which decreases the lexicographic measure M, guaranteeing forward movement and preventing deadlock. Well-Foundedness M = (k₁, k₂, k₃, k₄) where k₁ ∈ [0, |V|], k₂ ∈ [0, L·Rₘₐₓ], k₃ ∈ {0,1,2,3,4}, k₄ ∈ [0, max_batch_size] Lemma A.8.4: Each component of the lexicographic measure M is bounded and ranges over a well-ordered set, ensuring no infinite decreasing sequences exist. 9. Advantages The benefits of adopting the PDFD methodology are summarized in Table 36. 33 of 186 Table 36. Summary of design advantages offered by PDFD across validation, scalability, and completeness dimensions. Property Advantage Early Validation Depth-first traversal enables early detection of structural and behavioral issues in the hierarchy. Controlled Concurrency Parameter Kᵢ regulates concurrent workload distribution in real time. Targeted Refinement Parameter Rₘₐₓ bounds rework iterations per level, balancing precision and efficiency. Completeness Guarantee Combined bottom-up and top-down closure ensures that all components are fully processed. Scalable Design Dynamic parameters adapt traversal behavior to diverse tree structures. Hierarchical Closure Systematic traversal guarantees complete coverage from root to leaves. The full formal specification for PDFD is provided in Appendix A.6. 3.4.2. Primary Breadth-First Development (PBFD) This section presents Primary Breadth-First Development (PBFD), a hybrid methodology for complex hierarchical system development. PBFD combines pattern-driven breadth-first progression with selective depth-first traversal and robust cyclic refinement mechanics. It incorporates certain foundational concepts established in PDFD (Section 3.4.1) while introducing pattern-based modularity for managing architectural complexity. 1. Definition and Pattern Encapsulation PBFD operates over a hierarchical structure of L levels (L ≥ 1), where nodes at each level i are collectively denoted as level(i) [58]. Each node n maintains a processing state P(n) ∈ {0, 1, 2}, with P(n) = 2 indicating finalized status. To operationalize pattern-based modularity, PBFD employs hierarchical encapsulation mechanisms, realized in this study as Three-Level Encapsulation (TLE). TLE is a structural schema that encapsulates exactly three hierarchical levels into a single processing unit. Each node is a constituent component of a TLE pattern instance, and can serve as the anchor for a subsequent instance. This anchoring creates a continuous chain of dependency, allowing the methodology to enforce local consistency while traversing the global hierarchy. Example: Consider a geographic hierarchy (Continent → Country → State → County → City): • Instance 1 (Continent-anchored): Continent → Country → State • Instance 2 (Country-anchored): Country → State → County • Instance 3 (State-anchored): State → County → City Core Paradigms The methodology synthesizes three core paradigms: • Breadth-First Development (BFD): PBFD's primary progression is breadthfirst, facilitating sequential, level-by-level processing of the layered directed acyclic graph. Nodes within the same level share structural characteristics defined by discrete structural signatures (e.g., bitmask encoding), enabling efficient pattern-driven initial development and horizontal batch processing. Because BFD processes nodes level-by-level, a single pattern implementation is reused across all nodes sharing the same signature (e.g., bitmask-defined level sets, shared data schemas, or common processing logic). • Depth-First Development (DFD): DFD complements the breadth-first structure by enabling selective vertical traversal. Within TLE structure, DFD is operationalized through selective promotion of parent nodes to grandparent positions. This allows the system to refine specific hierarchical paths (critical subtrees) without processing all branches uniformly. 34 of 186 • Cyclic Directed Development (CDD): CDD governs validation-driven refinement by introducing bounded iterative cycles. This permits systematic re-entry into development based on feedback, continuing until predefined resolution criteria or refinement limits are met [78]. Pattern-Driven Progression • Selection and Advancement: At level i, specific patterns (denoted Patternᵢ, a subset of nodes at level i; see Table A.1.4) are selected and processed based on dependency structure or criticality [65,79]. Advancement to level i+1 is permitted only when all nodes within Patternᵢ reach finalized status (P(n) = 2), enabling the derivation of Patternᵢ₊₁ from the children of those finalized nodes. • Selective Refinement: Pattern progression to Patternᵢ₊₁ is governed by selective advancement via function select_critical_children(Patternᵢ) (Table A.1.5). This mechanism concentrates refinement along critical paths while preserving completeness guarantees through the S₄ completion phase (Table 39). This modularity follows principles of minimizing coupling and maximizing cohesion [80]. • Implementation Optimization: To handle the complexity of overlapping patterns, the PBFD MVP implementation utilizes TLE with bitmask encoding (Section 4), which support O(1) updates and minimize data-access coupling [53, 55]. Refinement Mechanism • Validation-driven refinement: Upon validation fails at level i, the function trace_origin(i) identifies the earliest affected level Jᵢ. This triggers reprocessing across the range [Jᵢ, i]. This backtracking capability allows previously finalized nodes to be revisited when validation errors originate from earlier levels, ensuring systemic coherence and architectural integrity across the hierarchy [82]. • Bounded refinement: CDD enforces the per-level limit Rₘₐₓ and iteration tracking indices—adhere to the formal model introduced in PDFD (Section 3.4.1), enforcing termination consistent with lifecycle principles [83]. The PBFD MVP implementation demonstrates this with Rₘₐₓ = 50 (Appendix A.14). Completion Phase • Top-down finalization: Upon reaching the leaf level, PBFD initiates a top-down completion phase [81]. Remaining unprocessed patterns are finalized sequentially from level 1 through level L. This ensures comprehensive system completion while preserving the architectural consistency established during patterndriven progression. Theoretical Grounding PBFD's pattern-driven approach aligns with established software architecture paradigms [65] and extends the formal control mechanisms of PDFD to support modular, incremental development of complex hierarchical systems. The selective depth-first elaboration balances breadth-first architectural visibility with targeted vertical refinement, optimizing for both cognitive manageability and architectural coherence. Formal Parameters The key parameters of PBFD are summarized in Table 37. Table 37. Control parameters used in PBFD: Key parameters guiding progression, validation, and refinement across hierarchical levels. Symbol Description L Maximum depth (leaf level) of the hierarchical tree Jᵢ Start of refinement: Earliest level impacted by failures in Patternᵢ (at level i), computed via trace_origin(i) (see PDFD, Section 3.4.2) 35 of 186 Note: Rₘₐₓ specifies the maximum number of collective attempts allowed for all patterns within a given level, rather than for individual patterns. 2. Key Characteristics PBFD’s structural and functional behavior is summarized in Table 38. Table 38. Key Characteristics of PBFD: Summary of pattern-driven traversal, depth transition, and completion behavior. Characteristic Description Theoretical Basis / Inspiration Pattern-Driven Traversal Nodes are grouped into patterns and processed level-by-level, with selective advancement to critical child nodes at each step, and may be optimized for O(1) data-access efficiency using techniques like bitmask encoding. Breadth-First Search (BFD), Architectural Patterns [79, 84, 85] Depth Transition Children of current pattern nodes are promoted as the next pattern (Patternᵢ₊₁) Dependency Tracing [65], DFD Principles Pattern-Based Refinement On validation failure, PBFD rewinds to prior levels (Patternⱼ) to correct impacted nodes. Example: Reprocessing level 1’s “data access” pattern due to a failure in level 2’s “security” pattern. Iterative Development, Feedback Loops (CDD) [78], Software Evolution [86] Parallelism Nodes within a pattern are processed concurrently. Advancement to the next state occurs only after all processed nodes within the pattern are successfully validated. Scalable Parallelism, Horizontal Concurrency Top-Down Finalization Finalization iterates from the root (level 1) to the leaf level (L), ensuring all dependencies are resolved and complete processing from root to leaves is achieved. Top-Down Validation, Structured Design [81] Termination Guarantee Process termination is guaranteed once all required conditions are satisfied, considering bounded refinements and finite tree structures. Formal Methods, Well-Founded Measures [61], Model Checking (CSP/SPIN) [71, 45, 87] Patterns such as “security” or “logging” may be compactly represented as bitmasks, enabling parallel resolution or traversal via techniques like Three-Level Encapsulation (TLE) [53,55] (see Section 4). 3. Workflow Representation Figure 12 illustrates the full PBFD workflow, including horizontal pattern processing, depth-based transitions, validation-triggered refinement loops, and the finalization phase. Figure A.14.1 in Appendix 14 is an example of data driven PBFD workflow where the development node is the row data. The corresponding source code is available in Appendix A.7.1. Symbol Description Rᵢ Refinement range: Number of levels (Rᵢ = i - Jᵢ + 1) to reprocess, spanning patterns from level Jᵢ to i, bounded by L Rₘₐₓ Iteration limit: Maximum refinement attempts per level (Patternⱼ), matching PDFD’s per-level refinement cap (Section 3.4.2) Patternᵢ A formal model: A cohesive, feature/function-grouped subset of nodes (data, logic, UI artifacts) at hierarchical level i, encapsulating a distinct unit of business logic [79, 80, 84]; Patternᵢ₊₁ is a selected subset of ∪_{n∈Patternᵢ} children(n), chosen based on critical path, dependencies, and development priorities rⱼ Current refinement attempt index for Patternⱼ 36 of 186 Figure 12. PBFD Structural Workflow: Hierarchical traversal, refinement feedback loops, and finalization path. Description: The diagram presents a tree-like hierarchy of nodes partitioned into level-wise patterns. Each Patternᵢ is processed horizontally before deriving the next level’s pattern from the children. Nodes failing validation generate feedback that rewinds execution to a prior Patternⱼ, triggering refinement. After reaching the leaf level, unprocessed nodes across all levels are finalized via top-down traversal. 4. State Descriptions PBFD’s behavior is formally captured via a set of states, described in Table 39. Table A.14.1 of Appendix A.14 is an instance of the PBFD state description in a PBFD MVP. Table 39. State definitions for PBFD: Operational phases during pattern processing, validation, refinement, and completion. State ID Phase Description S₀ Initialization Load tree and initialize patterns S₁(i) Current Pattern Processes nodes in Patternᵢ S₁(i+1) Next Pattern (Children) Represents the state of actively processing Patternᵢ₊₁, which is derived from children of Patternᵢ S₁(j) Refinement Level Reprocess Patternⱼ due to failure propagated from a later level S₂(i) Pattern Validation Validate processed nodes in Patternᵢ S₂(j) Refinement Validation Validate reprocessed nodes in Patternⱼ during refinement S₃(i) Depth-Oriented Resolution Depth-Oriented Resolution (Normal Context) - Load required data and resolve node implementation before descending S₃(j) Refinement Depth-Oriented Resolution Refinement Depth Resolution - Load required data and resolve node implementation for Patternⱼ during refinement before descending or returning to the original context S₄(i) Completion Level Finalize unprocessed nodes in Patternᵢ during the top-down pass S₅ Error Terminates due to unresolved validation failures after exhausting Rₘₐₓ T Termination All patterns processed and finalized 37 of 186 5. Unified State Transition Table Table 40 defines the unified transition logic for PBFD, mapping each workflow rule to a formal condition and state transition. Note that while the state machine diagrams use simplified labels for readability, the transition conditions in this table remain the formal, detailed specifications. Definitions for predicates and functions used in the table are provided in Table A.1.5 and A.7.1. Table A.14.2 of Appendix A.14 is an instance of the PBFD state transition table in a PBFD MVP. Table 40. Unified PBFD state transition logic: Workflow rules mapped to conditions and operational state progressions. Rule ID Source State Target State Condition Operational Step PB1 S₀ S₁(i) i = 1 Begin pattern processing at root level PB2 S₁(i) S₂(i) ∃n ∈ Patternᵢ: ¬validated(n) Validate current pattern nodes PB2a S₁(i) S₃(i) ∀n ∈ Patternᵢ: validated(n) Current pattern processing successful; proceed to depth resolution PB3 S₂(i) S₁(j) (∃n ∈ Patternᵢ: ¬validated(n)) ∧ j = trace_origin(i) ∧ refinement_attempts(j) < Rₘₐₓ Backtrack to level j and begin refinement PB3a S₁(j) S₂(j) ∃n ∈Patternⱼ: ¬validated(n) Validate Patternⱼ again after refinement (𝑒𝑥𝑝𝑙𝑖𝑐𝑖𝑡 𝑣𝑎𝑙𝑖𝑑𝑎𝑡𝑖𝑜𝑛 𝑝𝑎𝑡ℎ)(1) PB3a1 S₂(j) S₃(j) ∀n ∈ Patternⱼ: validated(n) Resume depth resolution after refinement PB3a2 S₂(j) S₁(j) ∃n ∈ Patternⱼ: ¬validated(n) ∧ refinement_attempts(j) < Rₘₐₓ Retry refinement processing at level j PB3a3 S₂(j) S₅ ∃n ∈ Patternⱼ: ¬validated(n) ∧ refinement_attempts(j) ≥ Rₘₐₓ Terminate due to unresolved validation failures after exhausted refinement attempts PB3b S₁(j) S₃(j) ∀n ∈ Patternⱼ: validated(n) Refinement validated; proceed to resolve depth of the finalized nodes (P(n)=2) in level j PB3c S₂(i) S₅ (∃n ∈ Patternᵢ: ¬validated(n)) ∧ (trace_origin(i) undefined ∨ refinement_attempts(trace_origin(i)) ≥ Rₘₐₓ) Terminate due to Patternᵢ has unvalidated nodes but refinement is impossible PB4 S₂(i) S₃(i) ∀n ∈ Patternᵢ: validated(n) Proceed to resolve depth and prepare next PB4a S₃(i) S₁(i+1) i < L ∧ Patternᵢ₊₁ ≠ ∅ Patternᵢ₊₁:= select_critical_children(Patternᵢ); Recurse to level i+1 for processing PB4b S₃(i) S₄(1) i=L ∨ Patternᵢ₊₁ = ∅ Transition to top-down finalization (prematurely or at leaf) PB5 S₃(j) S₁(j+1) j<i Resume pattern processing at next level within refinement scope PB6 S₃(j) S₃(i) j=i Refinement range complete; return to original current level for forward pass continuation PB7 S₄(i) S₄(i+1) ∀n ∈ Patternᵢ: processed(n) All nodes at level i finalized; move to level i+1 PB7a S₄(i) S₁(j) ∃n∈Patternᵢ:¬processed(n)∧j=trace_origin(i)∧refinement_attempts(j)< Rₘₐₓ Backtrack from completion phase to refinement processing PB7b S₄(i) S₅ ∃n∈Patternᵢ:¬processed(n)∧¬(j=trace_origin(i)∧refinement_attempts(j)< Rₘₐₓ) Terminate due to unprocessed nodes with no refinement options 38 of 186 Rule ID Source State Target State Condition Operational Step PB8 S₄(L) T ∀i ∈ [1, L], ∀n ∈ Patternᵢ: validated(n) All nodes completed PB9 S₁(j) S₅ refinement_attempts(j) ≥ Rₘₐₓ Terminate due to refinement cycle exhaustion Note: (1). Explicit validation again (PB3a) ensures corrections in parallel-processed patterns are synchronized before progression. Applies to both initial refinement entry (PB3) and retries (PB3a2). 6. State Machine Diagram Figure 13 presents the PBFD state machine, representing the operational semantics of the methodology, including pattern transitions, validation and refinement feedback, depth resolution, and top-down completion. This diagram provides a visual representation of the workflow described in Table 40. The corresponding source code is available in Appendix A.7.2. Figure A.14.2 of Appendix A.14 is an instance of the PBFD state machine diagram in a PBFD MVP. Description: The diagram shows transitions from initialization (S₀) into pattern processing states S₁(i), where patterns are validated (S₂) and resolved (S₃) before producing the next pattern. Validation errors may initiate a return to prior pattern levels for refinement (S₁(j)). Upon reaching the final level, the workflow transitions to S₄(i) for top-down finalization, terminating at T when all nodes are processed. Validation failures that exceed Rₘₐₓ refinement cycles transition to an error state (S₅), halting automated execution. 7. CSP Formal Verification Results and Refinement Guarantees This section confirms that the CSPM model (see Appendix A.7.4) of PBFD satisfies all formal refinement properties when verified using the FDR model checker. The verification (see Table 41) ensures the concrete implementation adheres strictly to the behavioral constraints, liveness properties, and robustness required by the PBFD specification, especially against an adversarial environment. Table 41. Formal Verification Results for PBFD Model. Property CSP Assertion FDR Result Engineering Significance Core Safety System: [deadlock free] ✓ Passed Prevents premature halts Core Liveness System: [divergence free]; SystemSync: [divergence free] ✓ Passed Eliminates infinite internal cycles Initialization Safety S0: [deadlock free]; S1_InitialProcess(L1): [deadlock free] ✓ Passed Confirms PB1 startup behavior from Table 40 Hostile Robustness HostileSystem: [deadlock free]; HostileSystemSync: [deadlock free] ✓ Passed Ensures correctness under non-cooperative inputs Conditional Consistency LegalCondEnv [T = NoContradictions] ✓ Passed Verifies mutual exclusivity across all decision predicates State-Level Safety 26 assertions ✓ Passed All operational and terminal states (S0–S5, T) verified across all level combinations Interpretation & Contributions Exhaustive State Coverage The 26 state-level assertions span every defined state in Table 39, including: • Initialization (S0, S1 at each level L1, L2, L3) • Validation (S2_ValidationInitial and S2_ValidationRefinement for all valid (j,i) combinations) • Depth progression (S3_DepthProgression and S3_RefinementDepthResolution for all valid (j,i) combinations) • Completion (S4 at all levels L1, L2, L3) • Terminal states (S5 for error, T for success) 39 of 186 Figure 13. PBFD state machine: Formal transition diagram covering initialization, pattern processing, refinement, and top-down finalization. 40 of 186 Each state was proven both deadlock-free and divergence-free for all legal trace origins and conditional environments. Termination via Rₘₐₓ The liveness checks confirm that no refinement loop can continue indefinitely. Transition rules PB3a3, PB7b, and PB9 from Table 40 enforce the bound on refinement attempts, ensuring the process always terminates at either T (success) or S5 (error). Robustness Against Adversarial Conditions Both hostile-environment assertions passed, confirming that PBFD's logic remains safe even when environmental conditions resolve in the least favorable (but legal) way. This validates that the state machine correctly handles all possible condition combinations. Implementation Fidelity All nine transition rules (PB1–PB9) from Table 40 execute as specified, with correct handling of per-level refinement, condition evaluation, and propagation through child nodes. Practical significance The verification results confirm that PBFD delivers production-grade reliability through the following guarantees: • Guaranteed Termination: The process always reaches either T (success) or S5 (controlled failure), eliminating the risk of system hangs. • Bounded Recovery: Infinite refinement cycles are prevented via enforcement of the Rₘₐₓ threshold, ensuring resource-bounded execution. • Fault Tolerance: The model maintains correctness under adversarial inputs, supporting deployment in mission-critical environments. Together, these guarantees ensure that a PBFD implementation cannot hang, enter an inconsistent conditional state, or exceed its refinement budget—regardless of input environment or traversal depth. 8. LTL Properties PBFD’s correctness is grounded in the properties defined in Table 42. Measure Argument: The termination and liveness proofs rely on a lexicographic measure M = (k₁, k₂, k₃, k₄) where: - k₁: Count of unfinalized nodes (k₁ = |{n ∈ G | P(n) ≠ 2}|) - k₂: Remaining refinement attempts across levels (decreases during refinement attempts) - k₃: Phase ordinal (Initialization S₀=4, Progression S₁=3, Validation S₂=2, Resolution S₃=1, Completion S₄=0) (decreases during forward phase transition) - k₄: Intra-phase progress measure (e.g., progress within S₁, S₃, or S₄ steps) Every non-terminal transition ensures a strict lexicographic decrease in M, as proven in Lemma A.8.7. Table 42. PBFD LTL Properties: Correctness guarantees, refinement bounds, and termination invariants. Property Formal Specification Description & Justification Total Correctness □(start ⇒ ((T ∧ Structural Invariants ) ∨ S₅)) Theorem A.8.8: The methodology always terminates (T or S₅), and, upon successful termination (T), guarantees that all nodes are validated and all structural invariants are satisfied. Termination □(start ⇒ ◊(T ∨ S₅)) Lemma A.8.4: Always, if the system starts, it eventually reaches the successful Termination (T) or bounded Error (S₅) state [61]. Well-Foundedness M = (k₁, k₂, k₃, k₄) where k₁ ∈ [0, |V|], k₂ ∈ [0, L·Rₘₐₓ], k₃ ∈ Lemma A.8.4: Each component of the lexicographic measure M is bounded and ranges over a well-ordered set, ensuring no infinite decreasing sequences exist. 41 of 186 Property Formal Specification Description & Justification {0,1,2,3,4}, k₄ ∈ [0, max_batch_size] Bounded Refinement ∀k ∈ [1, L], □(refinement_attempts(k) ≤ Rₘₐₓ) Lemma A.8.2: The number of refinement attempts for any level (k) is strictly bounded by the constant Rₘₐₓ (e.g. Rₘₐₓ =50) [65,78]. A practical limit, such as Rₘₐₓ = 50, is used in the PBFD MVP implementation (Appendix A.14). Refinement Convergence □∀j:(refining(j) ⇒ ◊(¬refining(j)∨refinement_attempts(j) = Rₘₐₓ)) Lemmas A.8.2 & A.8.3: Each refinement cycle eventually resolves the issue or exhausts its attempt bound, ensuring refinement is not indefinitely stalled [78]. Finalization Monotonicity □((◯ k₁≤ k₁) ∨ (◯ k₁> k₁∧◯k₂ < k₂)) Lemma A.8.3: The global count of unfinalized nodes (k₁) is non-increasing. It strictly decreases during commit transitions (PB4a, PB7) and can only increase during a guarded, bounded refinement reset that is compensated by a strict decrease in k₂. Finalization Permanence ∀n∈G:□((P(n)=2∧¬∃j:(refining(j)∧n∈affected_nodes(j))) ⇒ ◯(P(n)=2)) Corollary A.8.3.1: A finalized node's status is permanent unless actively reset by a guarded, bounded refinement backtrack. Pattern Processing Order □∀i:((S₃(i)∧(i<L ∧ Patternᵢ₊₁ ≠ ∅)) ⇒ ◯(S₁(i+1))) Lemma A.8.6 (Level-wise Ordering Invariant): Progression to the next level's pattern (Patternᵢ₊₁) only occurs after the current pattern (Patternᵢ) is fully resolved. Top-Down Finalization Order □∀i:((S₄(i) ∧ (∀n ∈ Patternᵢ: processed(n))) ⇒ ◯S₄(i+1) ∨ ◯T ∨ ◯S₅) Lemma A.8.6 (Top-down Finalization Invariant): The completion phase strictly finalizes levels in sequence from root to leaf. [81]. Refinement Scope □∀i,j: (backtrack(i,j) ⇒ (j = trace_origin(i) ∧ j ≤ i)) Lemma A.8.6 (Refinement Locality Invariant): Backtracking always targets the calculated trace origin within the current progression frontier i, j ≤ i. Vertical Closure □((P(n)=2 ∧ children(n) ≠ ∅) ⇒ ♢(∀c ∈ children(n): P(c) ∈ {1,2} ∨ T ∨ S₅)) Implied by Lemma A.8.6 invariants: If a parent is finalized, its children are guaranteed to be addressed in the process flow, barring system termination. Global Consistency T ⇒ (∀n ∈ G, P(n)=2) Rule PB8 (Table A.8.3): Successful termination (T) guarantees that every single node in the system is finalized [88]. Soundness T ⇒ (∀n∈G: consistent(n) ∧ dependencies_satisfied(n)) Theorem A.8.8: Successful termination implies all nodes are internally consistent and satisfy their architectural dependencies. [88] Liveness (Progress) □((¬T ∧ ¬S₅) ⇒ ◯(M <_{lex} M)) Lemma A.8.7: From any non-terminal state, an enabled transition exists that strictly decreases the lexicographic measure M, guaranteeing forward movement and preventing deadlock. [61] Selective Progression Invariant □((state = S₃(i) ∧ i < L ∧ Patternᵢ₊₁ ≠ ∅) ⇒ ◯(state = S₁(i+1) ∧ Patternᵢ₊₁=select_critical_children(Patternᵢ))) Rule PB4a (Table A.8.3): Progression is guarded by the selection of the next pattern, ensuring only critical nodes are considered for the next processing cycle. Completion Phase Invariant □(state=S₄(i)⇒ (♢state=S₄(i+1) ∨ ♢T ∨ ♢S₅)) Rule PB7 (Table A.8.3): The sequential progression S₄(1) → S₄(2) → ... → S₄(L) ensures that finalization is strictly top-down for global completeness. 9. Advantages PBFD offers several advantages, as summarized in Table 43. Table 43. PBFD Advantages: Design benefits from hybrid traversal, modular patterning, and bounded refinement. Property Advantage Hybrid Flexibility Combines the strengths of breadth-first (BFD), depth-first (DFD), and cyclic refinement (CDD) models 48 of 186 • READ(Parent, Child): Check the state (selected/active) of a specific Child within a Parent's bitmask • WRITE(Parent, Child, State): Set or clear the state of a specific Child within a Parent's bitmask • COMMIT(Grandparent): Persist the updated TLE-encoded data for the grandparent context These operations can be composed into workflows suitable for various contexts (interactive web apps, batch data pipelines, streaming services, etc.). While this denormalized, bitmask-based representation resembles NoSQL’s document-oriented storage, the Three-Level Encapsulation (TLE) model is implemented entirely within a relational backend, preserving full ACID guarantees. This hybrid architecture is central to the PBFD MVP and the enterprise deployment: it achieves the scalability and traversal efficiency characteristic of NoSQL systems while maintaining the integrity and transactional reliability of relational databases. Performance Characteristics The TLE table's single-row, fixed-width representation of three-level subtrees eliminates multi-table joins and enables constant-time relationship queries. This structural compression—where an entire subtree maps to one table row with bitmask columns— directly produces the empirical performance gains reported in Section 5, where TLE-based queries consistently outperformed normalized designs. Key advantages: • Eliminated joins: Parent-child relationships accessed via bitmask operations within a single row • Predictable I/O: Fixed-width rows enable efficient memory layout and caching • Constant-time operations: Bitwise operations replace recursive traversals The hybrid architecture allows updates to flow through the normalized source table (preserving ACID properties) while reads leverage the optimized TLE representation (maximizing throughput). Synchronization between source and derived tables can be implemented via triggers, scheduled jobs, or event-driven updates based on consistency requirements. 4.2.3. Formal Specification and Verification Abstract State Descriptions The lifecycle for processing a hierarchical TLE data unit can be formally described by the abstract states outlined in Table 48. Table 48. Abstract state definitions for the TLE hierarchical data processing lifecycle. State Phase Abstract Description S₀ Idle The TLE structure is at rest; no active unit of work. S₁ Data Loaded A TLE data unit (e.g., a grandparent row) has been loaded into a processing context. S₂ Hierarchy Resolved The grandparent and parent levels have been identified and validated. S₃ Children Evaluated Child node states have been read and logically processed (e.g., filtered, validated). S₄ Children Updated Child node states have been modified via bitmask writes. S₅ Changes Committed All modifications to the TLE structure are persisted to the grandparent entity. S₆ Workflow Finalized The unit of work is complete; the system is ready for the next task (via transition TLE10 to S₀ in the CSP model to ensure system liveness). Unified State Transitions 49 of 186 Transitions between these abstract states are governed by TLE operations and business-logic conditions, detailed in Table 49. Definitions of all functions and variables referenced in this section are provided in Table A.9.1. Table 49. Formal state transition rules for the abstract TLE processing model, defining the lifecycle of hierarchical data operations and ensuring reproducibility of PBFD's traversal logic. Rule ID From State To State Transition Condition/Trigger Core TLE Operation/Action TLE1 [*] S₀ System Start - TLE2 S₀ S₁ initiate_workflow(Grandparent) LOAD(Grandparent) TLE3 S₁ S₂ resolve_hierarchy() (Internal resolution) TLE4 S₂ S₃ evaluate_children() Iterative READ(Parent, Child) TLE5 S₃ S₄ update_required ∧ apply_update() WRITE(Parent, Child, State) TLE6 S₃ S₅ ¬update_required - TLE7 S₄ S₅ persist_changes() COMMIT(Grandparent) TLE8 S₅ S₀ has_next_unit() - TLE9 S₅ S₆ ¬has_next_unit() - TLE10 S₆ S₀ Workflow Complete finalize_process() TLE11 S₀ S₆ ¬has_unprocessed_unit() - Conditions such as update_required represent atomic composite operations within the state machine. In the CSP specification (Appendix A.9), the S₆ → S₀ recursion (Rule TLE10) formally captures the readiness of the TLE engine for continuous, multi-unit processing. Figure 15 illustrates the state transitions from Table 49. Its source code is in Appendix A.9.2. This model represents the generalized lifecycle. Domain-specific implementations will provide the logic for the transition conditions. Formal Verification and Refinement Guarantees for TLE This section reports verification results using FDR 4.2.7. The analysis confirms conformance to the abstract model, correctness of parameterized state transitions, and safety of the event-driven execution workflow. The verification demonstrates that the TLE model preserves structural soundness, maintains isolation of per-unit processing, and supports continuous execution without deadlock or divergence (see Table 50). Table 50. Formal Verification Summary for TLE. Property CSP Assertion FDR Result Engineering Significance Core System Safety TLE_Process : [deadlock free], TLE_Process [T = TLE_Abstract_Process], TLE_Process [F = TLE_Abstract_Process], TLE_Process [FD = TLE_Abstract_Process] ✓ Passed (4) Confirms conformance to the abstract model and absence of halting executions; guarantees full behavioral refinement State-Level Reliability TLE_S0, TLE_S1.u1–u3, …, TLE_S6.u1–u3 (Implementation) TLE_Abstract_S0, TLE_Abstract_S1.u1–u3, …, TLE_Abstract_S6.u1–u3 (Abstract) ✓ Passed (38) Ensures deadlock freedom for all operational states across all unit parameters; validates unit-specific determinism Liveness Guarantees TLE_Process : [divergence free], TLE_Abstract_Process : [divergence free] ✓ Passed (2) Confirms absence of infinite internal activity; guarantees workflow continuity 50 of 186 Property CSP Assertion FDR Result Engineering Significance Composition & Robustness TLE_TwoUnits : [deadlock free], TLE_Abstract_TwoUnits : [deadlock free], TLE_Hostile_System : [deadlock free], TLE_HostileEnv : [deadlock free], TLE_Process : [deterministic [F]] ✓ Passed (5) Validates safe concurrent execution, robustness under adversarial inputs, and internal determinism of the TLE workflow Figure 15. Abstract state machine diagram for TLE processing, showing transitions between phases of hierarchical data operations. Interpretation and Technical Contributions State-Space Coverage The verification covers all 49 assertions across the parameterized TLE state space. The 38 state-level checks reflect: 38 = 2 × [(1 non-parameterized state S₀) + (6 parameterized states × 3 units)] Broken down: • Implementation specification: S₀ (1) + S₁–S₆ across u₁, u₂, u₃ (18) = 19 assertions • Abstract specification: Abstract_S₀ (1) + Abstract_S₁–S₆ across u₁, u₂, u₃ (18) = 19 assertions • Total: 19 + 19 = 38 Unit-Specific Determinism Execution for S₁(u) through S₆(u) is verified separately for u₁, u₂, and u₃. Parameterized channels ensure events advance only the corresponding state instance, preventing interference across concurrent units. 51 of 186 Recurrence Guarantee State S₆(u) transitions to S₀ via finalize_process.u, ensuring continued operation over unbounded streams of TLE units. Failures–Divergences Refinement Passing the FD refinement confirms alignment between TLE_Process and TLE_Abstract_Process, ensuring that all observable behaviors and refusal sets match their formal specification. Hostile-Environment Robustness Deadlock-freedom under adversarial or out-of-order event injection demonstrates that external disturbances cannot force the system into unschedulable states. Practical Significance The verification establishes the following guarantees: • Isolation: Parameterized state and channel definitions maintain separation between concurrent units. • Robustness: The system remains safe under adversarial scheduling or unexpected event ordering. • Event-Driven Correctness: Synchronization via parameterized channels mirrors the intended event-driven semantics. • Continuous Operation: The S₆ → S₀ recurrence supports unbounded execution without termination or deadlock. The TLE model has been formally verified for correctness, consistency, and termination, with grounded proofs establishing liveness and the absence of deadlocks and livelocks (full details in Appendix A.9.6). 4.2.4. Performance Characteristics and Complexity Analysis Computational Complexity The computational characteristics of TLE are derived from its bitmask-based representation and direct-memory semantics. These characteristics determine the operational complexity of core actions such as storage, lookup, update, and batch traversal. Table 51 summarizes the complexity guarantees formally proven in Appendix A.10 (Theorems A.10.1–A.10.4). These results quantify the performance behavior of TLE under varying hierarchical distributions. The core notation appears in Table A.1.8 of Appendix A.1. Table 51. Computational characteristics of the Three-Level Encapsulation (TLE) model, with complexity guarantees from Theorems A.10.1–A.10.4. Characteristic Operation /Complexity Explanation Storage Efficiency Storage ratio: 𝑆𝑇𝐿𝐸/ 𝑆𝑡𝑟𝑎𝑑𝑖𝑡𝑖𝑜𝑛𝑎𝑙 = Ć / (ĉ · k) Encodes child-relationship sets in bitmasks instead of foreign key rows. Ć = average bitmask size; ĉ = average children per parent; k = metadata overhead per relational child record. For sparse hierarchies where Ć ≪ ĉ · k, TLE yields substantial storage reduction. Query Complexity O(1) (n ≤ w), O(⌈n/w⌉) otherwise Bitmask lookup enables constant-time child existence checks when the hierarchy fits within a standard word size. Update Cost O(1) (n ≤ w), O(⌈n/w⌉) otherwise Updates (adding/removing child association) are performed via bitwise OR / AND / XOR instead of relational inserts/deletes. Batch Parent Traversal O(𝑃𝑡𝑜𝑡𝑎𝑙) A linear scan over all parent entities eliminates index lookups, since parent–child presence is determined from the mask. Denormalization Cost O(1) amortized There are no join tables, as relationships are encoded directly in each parent row. 52 of 186 TLE compresses hierarchical relationships into word-sized (or compactly encoded) bitmasks and performs direct bitwise computation without joins or secondary index scans. This yields constant-time operations when the hierarchy fits within a machine word and logarithmic scaling otherwise. These performance characteristics explain the empirical gains demonstrated in Section 5. Formal Properties The TLE model also exhibits properties beyond performance—specifically, properties related to semantics, correctness, and behavioral guarantees. These are summarized in Table 52 and supported by formal proofs in Appendix 10 and FDR model checking in Appendix 9. Table 52. Formal properties of Three-Level Encapsulation (TLE) model. Property Description Formal Basis Storage Efficiency Replaces O(m) foreign key storage with O(Σ Cᵢ) bitmask storage, yielding an asymptotic reduction of O(1/k). Sparse hierarchies amplify the reduction factor Theorem A.10.1 Query Complexity O(1) lookup of child-membership status when n ≤ w (word size) using bitwise tests; O(⌈n/w⌉) for larger hierarchies Theorem A.10.2 Update Complexity O(1) bitwise update on the mask; does not require relational mutations Theorem A.10.3 Batch Processing Direct sequential scan through bitmasks enables parent-level batch traversal in O(𝑃𝑡𝑜𝑡𝑎𝑙) Theorem A.10.4 Semantic Expressiveness Maintains explicit root → parent → child semantics; masks encode relationship cardinality constraints Section 4.2 (Figs. 14– 15), [96] Behavioral Correctness Verified deadlock-free lifecycle based on TLE state machine FDR4 Proof (Appendix A.9) Empirical Evidence Demonstrated significant storage savings and faster query execution at MVP and enterprise deployment scale Section 5 Unlike Table 51, which addresses computational cost, Table 52 synthesizes TLE’s ontological, behavioral, and correctness guarantees—demonstrating that TLE is not only efficient, but also semantically precise, verification-ready, and ACID compliant. 4.3. Summary of Advantages The key techniques and their advantages are consolidated in Table 53. Table 53. Summary of hierarchical encoding techniques and their benefits, highlighting their role in enabling PBFD's scalability, maintainability, and empirical performance gains (Section 5). Technique Purpose Role in Architecture Benefits Bitmask Encoding (4.1) Efficient node selection and state tracking Foundation: Encodes set membership at O(1) complexity Compact storage, constant-time operations, parallelizable Three-Level Encapsulation (4.2) Structured hierarchical data management Framework: Applies bitmask encoding to Grandparent-Parent-Children structure Eliminates joins, O(1) relationship queries, scalable design Note: TLE builds upon bitmask encoding, using it at the Children level to encode parent-child relationships within a three-tier relational structure. This layered architecture enables both the storage compactness of bitmasks and the structural efficiency of hierarchical organization. These encoding strategies underpin the scalability and maintainability demonstrated in PBFD’s empirical deployments. The compactness of bitmask encoding and the join elimination of TLE were direct contributors to the substantial reductions in development effort, execution latency, and storage requirements detailed in Section 5. Source code and the full formal specification for the described TLE operations are provided in Appendix A.9, ensuring reproducibility and facilitating integration into other hierarchical data systems. 53 of 186 5. Evaluation of PBFD and PDFD: From Controlled MVPs to Production Deployment We evaluated the Primary Breadth-First Development (PBFD) and Primary DepthFirst Development (PDFD) methodologies through a multi-method empirical strategy. This approach encompassed both the implementation of open-source Minimum Viable Products (MVPs) to validate the core architectural principles and a longitudinal case study of a production PBFD deployment to measure large-scale performance [97]. This evaluation advances Evidence-Based Software Engineering (EBSE) [98] by providing reproducible artifacts and empirical data. The MVP implementations ground the formal state transitions and methodological workflows in practical systems, extending the vision of improvement-oriented software environments [99]. Evidence from MVP Implementations The PDFD MVP (Appendix A.11) was essential for validating Hybrid Depth-First Progression (BF-by-Two) and demonstrated early conflict detection across sibling nodes—such as UI state inconsistencies between “Asia” and “North America”—that cannot be detected as early in pure depth-first strategy. It further operationalized bounded refinement (Rₘₐₓ = 60, chosen empirically) and iterative schema adaptation in response to mid-development changes. This was conducted as a controlled experiment, designed to test bounded refinement and sibling-node conflict detection under reproducible conditions. The PBFD MVP (Appendix A.14) served as a concrete instantiation of the Three-Level Encapsulation (TLE) architecture and bitmask encoding, providing a reproducible artifact that validated the core mechanisms enabling high performance. It demonstrated the replacement of four to five join traversals with direct one-hop access and confirmed the feasibility of constant-time (O(1)) bitmask updates under controlled conditions (See Table A.14.7). This was conducted as a controlled experiment, validating constant-time bitmask updates and one-hop access in a reproducible test harness. All MVP components—including schema generators, migration scripts, test harnesses, and sample datasets—are publicly available in the artifact repository [28,29], enabling third-party validation and replication under real-world conditions. From Architectural Validation to Production Performance The architectural patterns validated in the PBFD MVP—specifically TLE and bitmask-based subtree encoding—were directly deployed in the enterprise system. The production implementation subsequently recorded dramatic performance results, achieving 7–8× faster query execution and an 11.7× reduction in storage requirements compared to normalized relational designs. Development timelines were reduced by 20×, and zero post-release defects were recorded over eight years of continuous operation—outcomes attributable to the structured, constraint-driven application of PBFD. Focus of This Section While both methodologies were rigorously evaluated through their MVP implementations, this section emphasizes the longitudinal PBFD enterprise deployment. This case was selected for its scale, ecological validity, and availability of long-term operational data, enabling a comprehensive assessment of methodology impact on development effort, runtime performance, and storage efficiency in a real-world setting. All findings presented are derived from anonymized operational metrics and reproducible performance benchmarks collected over multiple release cycles over a span of eight years. 5.1. Problem Context A client required a claim form application to capture detailed incident reports, a domain characterized by high structural complexity [100]. The project faced three core challenges under an aggressive three-week delivery constraint: 54 of 186 • Complex data requirements: The system was designed to support the structured capture of incident locations, timelines, multi-tiered classification codes, and detailed employment data, including union affiliations, employment status, and employer information. • Deep hierarchical dependencies: The form structure includes up to eight levels of conditionally dependent elements, which are formally modeled as an n-ary tree. This depth leads to a combinatorial explosion of possible states, making traditional row-based storage and retrieval inefficient [91]. • Performance and Delivery Demands: The system required real-time validation and responsive user interaction under production load, with complete feature delivery within three weeks—a timeline incompatible with conventional iterative development approaches. Traditional relational approaches, reliant on normalized schemas and volumetric join operations, exhibited high latency and fragile scalability when maintaining consistency across these hierarchical layers [54], making them unsuitable for both the technical complexity and the compressed delivery schedule. 5.2. Solution: Adoption of PBFD Methodology To address these challenges, we adopted the PBFD methodology, leveraging its levelwise processing strategy and bitmask-based hierarchical encoding to achieve constanttime (O(1)) operations on hierarchical relationships [101]. The development process followed the structural workflow illustrated in Figure 12 and was guided by four key design principles: Hierarchical modeling The business logic was formally structured as an 8-level n-ary tree (Figure 16; Mermaid source code in Appendix A.19), providing a graph-based representation that enabled systematic decomposition of the domain’s hierarchical structure. This n-ary model allows PBFD’s bitmask encoding to capture complex parent–child relationships while maintaining (O(1)) query performance through ancestral path encoding. Figure 16. Eight-level n-ary business hierarchy for claimant management. The highlighted path (red nodes) traces the primary analytical chain from Claimant to Specific Metric. Green nodes represent 55 of 186 alternative branches—for example, multiple incident locations at Level 2 (N2_1, N2_2, N2_3) enable different analytical pathways. Bitmask-based representation Each user selection was stored as a compressed bitmask encoding aligned to its hierarchical level, applying the mechanism detailed in Section 4.1. This enabled efficient storage, traversal, and bitwise set operations (union, intersection, difference) on hierarchical selections [102]. Database Optimization via Consolidated TLE Schema The production deployment adapted the Three-Level Encapsulation (TLE) principles from Section 4.2 into a consolidated, high-performance schema. While the canonical TLE pattern uses one table per grandparent node to maximize theoretical extensibility, the production implementation collapses all nodes into two shared tables, trading structural flexibility for query performance and development simplicity. Consolidation Approach • Hierarchy flattening: The 8-level hierarchy (Figure 16) was flattened by representing grandparent entities as columns within a single table, rather than as separate tables in the canonical TLE design. This creates a recursive column promotion pattern: o Parent columns at level N contain bitmask values encoding their children o These parent columns are promoted to grandparent columns at level N+1 o Each column–bitmask pair preserves the parent→child relationship within a unified table structure For example, a “United States” column (grandparent) is associated with statelevel parent columns, which in turn store county-level bitmasks as children. At the next level, state columns are promoted to grandparent roles for their respective county hierarchies. This recursive promotion continues through level L-3 (where L is the total hierarchy depth), stopping two levels before the bottom to ensure sufficient depth for TLE encoding. • Preserved semantics: The core TLE logic remains unchanged—for any parent value, a bitmask column encodes its selected children. Parent–child relationship semantics and bitwise operations are identical to canonical TLE; only the physical storage model differs. • Performance outcome: This consolidation reduced the transactional schema to two tables, minimizing I/O overhead and join complexity while guaranteeing production-scale performance [54]. This adaptation demonstrates TLE’s flexibility: its core bitmask-based encoding supports both canonical multi-table schemas and consolidated wide-table designs, enabling performance-tuned deployments without sacrificing semantic integrity. UI integration Dynamic user interfaces directly interpreted bitmask-encoded data to render hierarchical form structures, ensuring consistency between the data model and presentation layer. 5.3. Implementation Outcomes The adoption of PBFD yielded significant improvements across key engineering metrics. Table 54 summarizes the results while detailed methods and evidence are in the appendices. To support methodological transparency and traceability, Table 55 expands on the study types listed in Table 54 by detailing their design dimensions and evaluation structure. 56 of 186 Table 54. Empirical results from a PBFD enterprise deployment, demonstrating improvements in development speed, runtime performance, and storage efficiency over traditional relational and OmniScript-based implementations. Aspect PBFD Outcome Reference & Notes Development Speed At least 9× faster than equivalent relational development and 20× faster than OmniScript; full-stack system delivered in 1 FTE-month Appendix A.20 — longitudinal observational study [103,104] Runtime Performance 7.64× faster (P50), 8.54× faster (P95); P5 equal to baseline (identical latency floor); sustained across 8 years Appendix A.21 — quasi-experimental runtime comparison under identical infrastructure [105,106] Storage Efficiency 11.7× less reserved space, 85.7× smaller index size, 113.5× better page utilization; eliminated junction tables Appendix A.22 — controlled schema-level evaluation comparing PBFD vs. normalized designs [105,107] System Stability Zero critical defects, deadlocks, or regressions across 8 years Internal monitoring; Longitudinal observational study [97] Onboarding Efficiency Junior developer delivered a production feature in one week Internal engineering metrics — qualitative observational evidence [107] Notes: Study types follow Evidence-Based Software Engineering (EBSE) guidelines [97, 105,107], distinguishing observational, quasi-experimental, and controlled design-science evaluations. Table 55. Experimental Designs Dimensions in PBFD Evaluation. Design Dimension Development Speed Runtime Performance Storage Efficiency Unit of Comparison Implementation methodology (PBFD vs. relational vs. OmniScript) Different UI endpoints within the same deployed application Different schema designs (TLE vs. normalized) within the same database Evaluation Focus Effort and time required to implement equivalent functionality Request latency and execution speed Reserved space, index size, and page utilization Controlled Variables Shared enterprise context, functional requirements, audit logging Same hardware and application context; workload varies by page logic Same DBMS, hardware, and data volume Independent Variable Development methodology and platform Page-level logic and rendering paths Schema structure (TLE vs. normalized joins) Study Type Longitudinal observational case study Quasi-experimental comparison Controlled schema-level experiment The findings from Table 54 confirm that PBFD reduces development effort, improves runtime responsiveness, and optimizes storage for hierarchical workloads—translating its theoretical advantages into sustained production impact. To clarify the methodological basis for each evaluation, Table 55 summarizes the experimental design dimensions and study types applied in the PBFD assessments. 5.4. Technical Observations Analysis of the production deployment yielded the following observations: • Rapid Development and Onboarding: PBFD enabled one developer to deliver a production system in a single month. Compared to traditional methods (≥9× faster) and low-code tools (≥20× faster), this is supported by Appendix A.20’s analysis. The graph-driven structure also fostered rapid onboarding, aligning with evidence on the role of coherent mental models in comprehension [108]. • Compact Storage and Schema Simplification: Encoding relationships into fixed-width bitmask fields reduced schema complexity from 13 tables (6 factor and 7 junction tables) to 2, while achieving 11.7× overall storage reduction and 85.7× index reduction (Appendix A.22). 57 of 186 • Optimized Write and Query Performance: Bitwise O(1) updates replaced traditional O(n) multi-row operations. This explains the 7–8× page-load improvement and lower tail latency (Appendix A.21), mitigating known bottlenecks in hierarchical queries [91]. • Production-Stable Hybrid Semantics: PBFD illustrates a hybrid relational– NoSQL design through TLE: SQL Server is used to achieve document-like modeling within a relational system. Eight years of production stability demonstrate that PBFD balances hierarchical flexibility with ACID integrity [109]. 5.5. Limitations and Threats to Validity While promising, the results must be qualified by the following threats [97]: • Single-case Generalizability: Findings from one enterprise case, offering strong ecological validity but limited statistical generalization • Construct Validity – Developer Expertise: While all implementations were led by expert developers, expertise levels and domain familiarity vary across individuals. The PBFD vs. relational comparison involves the same expert (PBFD's inventor) leading both, introducing additional confounds from learning effects and problem familiarity. Detailed analysis in Appendix A.20.5 • Construct Validity – Baseline Heterogeneity: Heterogeneous systems for baseline comparisons, providing ecological realism and potentially underestimating PBFD’s performance advantage (see Appendices A.21.6, A.22.4) • Temporal and Maturation Threats: Data spanning 2016–2024, introducing potential history and maturation effects mitigated by the longitudinal design These threats are explicitly addressed in the appendices. Broader replication studies are discussed as future work in Section 7. 6. PDFD AND PBFD Comparative Analysis This section evaluates the proposed Primary Depth-First Development (PDFD) and Primary Breadth-First Development (PBFD) methodologies in comparison to traditional Full-Stack Software Development (FSSD) approaches and modern database paradigms, with additional focus on hierarchical encoding techniques specific to PBFD. The comparative analysis is grounded empirically in Section 5 and Appendices A.11–A.22, including the detailed MVP comparisons in Appendix A.18, ensuring rigor and reproducibility. 6.1. Traditional FSSD: Situational Advantages and Trade-offs While PBFD and PDFD excel in complex hierarchical systems, traditional Full-Software Systems Development (FSSD) approaches may still be preferred in specific, less intricate scenarios. These traditional approaches align with established agile practices that emphasize iterative development and responsiveness to change [110]. Table 56 summarizes these situations and their associated trade-offs, providing a contextual comparison against established practices. Table 56. Situational trade-offs: Traditional FSSD versus PDFD and PBFD across selected project scenarios Scenario Traditional FSSD Advantage Trade-off with PDFD Trade-off with PBFD Small-Scale Projects Minimal setup and tooling overhead consistent with lightweight processes [111] Vertical slicing overhead unnecessary for trivial systems Hierarchical encoding and TLE architecture add unnecessary complexity. Rapid Prototyping Drag-and-drop tools quick iteration enabled Slower initial visibility due to vertical rigor Architecture-first planning delays visible prototypes. Non-Hierarchical Systems Works well for simple CRUD apps and dashboards Hierarchy modeling unnecessary Hierarchical encoding (TLE, bitmasks) provides no benefit. 64 of 186 Table 63. Preliminary mappings of TLE concepts for cross-paradigm investigation (speculative; requires empirical validation) Data Model Proposed TLE Mapping Key Research Question Document Database (MongoDB) Collection → Document → Nested bitmask fields Do MongoDB's bitwise operators ($bitsAllSet) provide query advantages over array-based flags, or do index scan costs outweigh storage benefits in row-oriented BSON? Key-Value Store (Redis) Key namespace prefix → Structured keys → Bitmask values Why does user→bitmask fail for cohort queries, and how does permission→bitmap achieve O(1) filtering with BITOP operations? Graph Database (Neo4j) Node labels → Node instances → Properties with bitmasks When do bitmask properties undermine index-free adjacency, and how do native edges preserve traversal performance? Formalizing these mappings and conducting comparative benchmarking across paradigms represent essential future research directions. Such studies would establish the generality of TLE's design principles, identify paradigm-specific performance trade-offs, and provide evidence-based guidance for practitioners selecting optimal platforms for hierarchical data processing at scale [90,113]. Until such empirical work is completed, TLE's benefits remain proven only in relational systems. 7.5. Relational Constraints and Design Trade-offs in PBFD Deployments PBFD’s relational implementation favors structural determinism over schema flexibility. Its Three-Level Encapsulation (TLE) replaces conventional junction tables with bitmask-encoded relationship fields, enabling constant-time hierarchy resolution within a compact, fixed schema. By removing multi-table joins and recursive queries, PBFD transforms relational traversal from O(n) joins to O(1) bitwise evaluations, yielding predictable and efficient execution paths. This optimization introduces deliberate constraints. Because hierarchical relationships are encoded rather than dynamically modeled, schema evolution requires controlled restructuring, limiting runtime flexibility. Likewise, PBFD delegates integrity management and relationship validation to application-level logic, minimizing reliance on stored procedures or foreign-key constraints. Despite these restrictions, PBFD remains fully compatible with native SQL query planners and indexing mechanisms. Its deterministic schema structure supports costbased optimization and stable execution plans, aligning with the principle that physical design must directly support the logical data model and workload characteristics to achieve efficiency [54, 118]. 7.6. Study Limitations This study is constrained by a limited number of in-depth case implementations. Comprehensive quantitative comparisons between PBFD/PDFD and traditional FSSD (e.g., latency, throughput) remain underexplored. Future work must prioritize systematic, controlled benchmarking under varied operating conditions—including workload diversity, concurrency levels, and schema complexity—for broader generalization [122,123]. 7.7. Unexpected Benefits Beyond primary objectives, post-deployment feedback revealed unanticipated benefits. PBFD’s clear separation of OLTP and OLAP workflows significantly improved operational clarity, streamlined data pipeline management, and enhanced reporting flexibility. This successful separation of concerns resonates with established database design practices for managing complex, high-throughput systems [54,118]. These advantages were particularly pronounced in large-scale claims processing, enabling cleaner architectural segregation and improved system resilience. 7.8. Additional Future Research Directions 65 of 186 Additional future research can further extend PBFD and PDFD's impact and applicability: • Domain Generalization: Extend methodologies to other contexts (e.g., ETL, BI, rules engines) by mapping abstract nodes to domain primitives and refining traversal semantics • Distributed and Modular Systems: Investigate utility in microservice and edge computing, focusing on runtime synchronization, orchestration, and modular validation • Tooling and Developer Ecosystem: Develop companion tooling (e.g., IDE plugins, visualizers) to translate abstract process models into accessible engineering workflows • Rigorous Empirical Validation: Conduct controlled comparative studies against conventional methods across performance, scalability, maintainability, and defect density. Future empirical work could build upon the comprehensive frameworks for evaluating database system performance as laid out in standard texts [54,118] This study positions PBFD and PDFD as formally grounded, empirically validated alternatives for FSSD. Despite initial adoption barriers and relational trade-offs, they demonstrate robust performance, maintainability, and efficiency in production. By generalizing these algorithms, enhancing developer tooling, and expanding empirical validation, future research can establish PBFD and PDFD as foundational paradigms for scalable, formally grounded software engineering. 8. Conclusion This paper introduces Primary Breadth-First Development (PBFD) and Primary Depth-First Development (PDFD)—formally grounded methodologies that address FullStack Software Development's persistent challenges in dependency management, hierarchical data efficiency, and cross-layer coordination. Built upon four foundational models (Directed Acyclic Development, Depth-First Development, Breadth-First Development, and Cyclic Directed Development), these approaches integrate graph traversal strategies, state machine workflow models, and bitmask-encoded data structures to provide rigorous foundations for hierarchical system development. Theoretical Contributions. PBFD and PDFD extend classical graph traversal with hybrid strategies offering provable termination under bounded refinement (Rₘₐₓ) and formal guarantees including deadlock freedom, dependency preservation, and finalization invariance. These properties are validated through Communicating Sequential Processes (CSP) and Linear Temporal Logic (LTL) specifications, with verification via FDR4 model checking. The Three-Level Encapsulation (TLE) pattern enables O(1) hierarchical operations through bitmask encoding, with complexity bounds proven in Theorems A.10.1– A.10.4 and operational correctness verified through CSP failures-divergences refinement. Empirical Validation. An eight-year production deployment of PBFD demonstrates exceptional reliability (zero critical failures) with substantial performance gains: over 20× faster development cycles, 7–8× faster query execution, and 11.7× storage reduction. These results, established through longitudinal observational studies, quasi-experimental runtime comparisons, and controlled schema-level experiments, confirm that formally verified, graph-based development can deliver measurable improvements in enterprise systems. Publicly available Minimum Viable Products ensure reproducibility and practical accessibility. Broader Impact. This work demonstrates that formal methods can enhance rather than hinder industrial software practice. PBFD and PDFD provide a practical pathway for 66 of 186 modernizing hierarchical enterprise systems with provable correctness while achieving significant performance improvements. The successful eight-year deployment establishes that verification-driven development and industrial pragmatism are not opposing forces but complementary approaches to building reliable, scalable systems. Future Directions. Key research avenues include cross-paradigm generalization (NoSQL, graph databases), automated tooling for pattern-driven development, and expanded empirical evaluation across diverse enterprise contexts. By advancing the rigor, efficiency, and scalability of complex system development, PBFD and PDFD lay groundwork for broader adoption of formally grounded methodologies in industrial software engineering. Acknowledgments The author gratefully acknowledges the support of IBM managers Jen Kostenko, Ricardo Zavaleta Cruz, and Anton Cwu for facilitating the publication process and for reviewing and authorizing the inclusion of the enterprise deployment case study materials used in this work. Portions of this manuscript benefited from AI-assisted editing tools used solely to improve clarity, consistency, formatting, and code debugging. All conceptual contributions—including research design, ideas, interpretations, analyses, and conclusions—are entirely the author's own. Data Availability Statement All non-proprietary data supporting the findings of this study are openly available. MVP implementations, formal specifications (CSP/CSPM models), validation datasets, and supplementary materials are available at https://github.com/IBM-Consulting-Formal-Methods. Additional detailed results, transition tables, and validation outcomes are provided in the manuscript appendices. The raw enterprise deployment data from the eight-year IBM case study is proprietary and cannot be publicly released due to client confidentiality agreements; the experimental environment, aggregated performance metrics, and a representative high-level technical architecture are included in the manuscript. Author Contributions Conceptualization, D.L.; methodology, D.L.; software, D.L.; validation, D.L.; investigation, D.L.; writing—original draft preparation, D.L.; writing—review and editing, D.L.; visualization, D.L. All authors have read and agreed to the published version of the manuscript. Funding This research received no external funding. Institutional Review Board Statement Not applicable. Informed Consent Statement Not applicable. Conflicts of Interest The author is an employee of IBM Consulting and declares inventorship of PBFD and PDFD. 67 of 186 Appendices A.1 Formal Notation and Semantic Symbols This appendix defines the logical and algebraic notations used throughout the formal models of Directed Acyclic Development (DAD), Breadth-First Development (BFD), Depth-First Development (DFD), Cyclic Directed Development (CDD), Primary DepthFirst Development (PDFD), and Primary Breadth-First Development (PBFD). Table A.1.1. Logical and Temporal Operators Symbol Meaning □φ Always φ (globally true) — “Globally” in LTL ◯φ Next state φ — φ will be true in the very next state ◊φ Eventually φ — φ will be true at some future time φ ⇒ ψ Implication — if φ holds, then ψ must also hold ¬φ Negation — φ does not hold φ ∧ ψ Conjunction — both φ and ψ hold φ ∨ ψ Disjunction — at least one of φ or ψ holds <_{lex} Lexicographical comparison. The operator evaluates if the tuple on the left is strictly less than the tuple on the right. Comparison proceeds from left to right, element by element. Table A.1.2. Quantifiers and Set-Based Expressions Expression Meaning ∀x ∈ X Universal quantifier: for all x in set X ∃x ∈ X Existential quantifier: there exists x in set X ∄ There does not exist (e.g., no cycles, no path) X ⊆ Y Set inclusion: X is a subset of Y X ∖ Y Set difference: elements in X but not in Y Table A.1.3. Process State Notation Notation Meaning P(n) = 0 Node n is unprocessed P(n) = 1 Node n is in progress P(n) = 2 Node n is fully processed and validated processed(n) P(n)=1 or P(n)=2 validated(n) P(n) = 2 finalized(n) P(n) = 2. Used interchangeably with validated(n) Table A.1.4. General / Mathematical Definitions This table defines fundamental concepts from graph theory and universal mathematical properties used throughout the methodologies. Term Definition / Description G=(V,E) A Directed Acyclic Graph (DAG) with vertex set V and edge set E children(v) The set of direct successor nodes to node v in the graph or tree D(v) Direct dependencies of node v: the set of nodes u such that there is a directed edge from u to v (i.e., {u | (u,v) ∈ E}) Tr Rooted, finite, acyclic tree structure with nodes V and edges E Cᵢ The current node being processed in the traversal Bⱼ A backtrack point (a node on the current path with unvisited siblings) Q Global queue tracking nodes to process Nₖ Set of nodes at level k 68 of 186 Term Definition / Description Iₖ Incremental delivery milestone k, representing a validated subset of the system Fₖ Feedback trigger mechanism (e.g., validation failure, stakeholder input) associated with milestone k depth(v) The length of the longest path from a root node to node v ancestors(v) The set of all nodes from which node v is reachable in the graph (i.e., {u ∈ V | there exists a path from u to v}) descendants(v) The set of all nodes reachable from node v in the graph (i.e., {u ∈ V | there exists a path from v to u}) level(k) The set of all nodes at a specific depth k in a tree or layered graph (i.e., {v ∈ V | depth(v)=k}) Path(v) A directed path from a root node to node v state(Bⱼ) A function mapping node Bⱼ to its processing state Subtree(Bⱼ) All descendants of node Bⱼ invalid(s) True if state s violates the state machine constraints or invariant conditions ReachableStates The set of all states reachable from the initial state through legal transitions follows_rules(t) True if the transition t complies with the transition rules consistent(n, a, d) True if node n is consistent with its ancestor a and descendant d in terms of structure/data valid_state(s) A state is considered valid if and only if it is not invalid(s) succ(L) Returns the successor level to L pred(L) Returns the predecessor level to L Next(level) Returns the logically next level from the current level (e.g., level + 1), capped at the maximum depth L. Used for sequential level progression Patternᵢ A formal model: a cohesive, feature/function-grouped subset of nodes (comprising data, logic, and UI artifacts) at hierarchical level i, encapsulating a distinct unit of business logic or system functionality (See Section 3.4.2 for detailed discussion) roots(G) The set of root nodes in graph G: {v ∈ V | ¬∃u: (u,v) ∈ E} leaves(G) The set of leaf nodes in graph G: {v ∈ V | ¬∃u: (v,u) ∈ E} L The maximum depth of the graph/tree hierarchy: max{depth(v) | v ∈ V} [P] Iverson bracket: [P] = 1 if predicate P is true, 0 otherwise bitmask Binary representation of child relationships under a parent, supporting constant-time access Table A.1.5. Core Definitions for Formal Methodologies: Predicates, Functions, and Constants This table serves as a central reference, defining the fundamental predicates, functions, and constants utilized in the formal specifications and particularly in the transition conditions across all methodologies. Term Type Description Methodologies processed(n) Predicate Evaluates to True if node n has undergone its core processing or development action DAD, DFD, BFD, CDD Rₘₐₓ Constant The maximum number of refinement attempts allowed for any specific level or pattern before an error state is triggered PDFD, PBFD Jᵢ Constant Start of refinement: Earliest level impacted by failures at i, where Jᵢ = trace_origin(i) PDFD, PBFD Rᵢ Constant Refinement range: The number of levels to reprocess, calculated as Rᵢ = i - Jᵢ + 1 (bounded by L) PDFD, PBFD Kᵢ Constant Progression Threshold: Minimum finalized nodes (P(n)=2) at level i required before advancing to i+1. Acts as a configurable WIP limit enforcing structured synchronization points PDFD, PBFD rⱼ Constant Current refinement attempt index for Patternⱼ PDFD 69 of 186 Term Type Description Methodologies Reset(n) Predicate Evaluates to True if node n's processing status or validation state is reverted, requiring re-evaluation or re-processing. PDFD, PBFD refinement_attempts(j) Counter Tracks the number of refinement attempts for a specific level/pattern j. Resets when a new refinement cycle begins PDFD, PBFD trace_origin(i) Function Determines the root cause level Jᵢ (or pattern Jᵢ) based on a validation failure detected at level i PDFD, PBFD trace(i) Function The path or sequence of levels leading to level i, used to constrain progression and ensure bounded advancement PDFD selected_subtree Set The subset of nodes selected for processing within a level or pattern, constrained by trace and eligibility criteria PDFD max_batch_size Constant The maximum number of nodes that can be processed in a single batch within a level PDFD validated(n) Predicate Evaluates to True if node n has successfully passed all its associated validation criteria DFD, BFD, CDD, PDFD, PBFD critical(n) Predicate True if node n requires vertical processing (children must be processed) PBFD start(i) Pseudocode Initial state transition (idle → active) DAD, DFD, BFD, CDD terminate(i) Pseudocode Terminal state (all nodes processed) DAD, DFD, BFD refine(c) Function A node that needs iterative improvement. CDD finalize(i) Function Finalizes a single node CDD processing_complete(i) Predicate Evaluates to True when processing at level i is complete PDFD refining(j) Predicate True when the system is executing a refinement cycle targeting level j (state = S₁(j) ∧ refinement_attempts(j) > 0) PDFD, PBFD affected_nodes(j) Function Returns the set of nodes {n ∈ G | ∃k ∈ [j, L]: n ∈ level(k)} that may be reset during refinement at level j PDFD, PBFD consistent(n) Predicate True if node n satisfies all internal consistency constraints and validation criteria specific to its domain PDFD, PBFD dependencies_satisfied(n) Predicate True if node n satisfies all architectural dependencies and interface contracts with related nodes PDFD, PBFD all_descendants_validated(n) Predicate True if all descendant nodes of n have been validated PDFD, PBFD processed_subtree(n) Function Returns the set of nodes selected for processing in the subtree of n PDFD, PBFD dequeue(v) Predicate True when node v is dequeued for processing DAD process(v) Function Initiates core processing for node v DAD select_critical_children(Patternᵢ) Function Returns a subset of ∪_{n∈Patternᵢ} children(n) selected based on critical path analysis, dependency ordering, and resource constraints. Ensures architectural coherence while allowing efficient progression, with remaining nodes handled in S₄ completion phase PBFD k₁ (unfinalized_nodes) Function Returns the count of nodes with P(n) ≠ 2 PDFD, PBFD k₂ (remaining_attempts) Function Returns ∑_{j∈ActiveLevels} (Rₘₐₓ − refinement_attempts(j)) PDFD, PBFD k₃ (phase_ordinal) Function Maps state phases to ordinals: S₀ = 4, S₁=3, S₂=2, S₃=1, S₄=0 PDFD, PBFD k₄ (intra_phase_progress) Function Tracks progress within the current phase PDFD, PBFD M Function Lexicographic measure M = (k₁, k₂, k₃, k₄) PDFD, PBFD 70 of 186 Term Type Description Methodologies enabled_transition(s) Predicate True if at least one transition is enabled in state s PDFD eligible(n) Predicate True if node n meets all local validation and architectural criteria, allowing it to be part of the set considered for the 𝐾ᵢ threshold in S₂ progression. (Implies validated(n) and consistent(n)) PDFD Structural Invariants Set/Term The set of all fundamental structural properties required for correct termination, including: Global Consistency, Descendant Finalization Invariant, and dependencies_satisfied for all nodes PDFD, PBFD test_failed(Cᵢ) Predicate True if testing of node Cᵢ fails CDD feedback_triggered(Cᵢ) Predicate True if feedback is triggered for node Cᵢ CDD refinement_complete(Cᵢ) Predicate True if refinement of node Cᵢ is complete CDD refinement_failed(Cᵢ) Predicate True if refinement of node Cᵢ fails CDD refinement_count(Cᵢ) Counter Tracks the number of refinements for node Cᵢ CDD all_components_written(Iₖ) Predicate True if all components in milestone Iₖ are written CDD feedback_received(Iₖ) Predicate True if feedback is received for milestone Iₖ CDD validation_failed(Iₖ) Predicate True if validation of milestone Iₖ fails CDD all_increments_validated Predicate True if all increments are validated CDD validation_successful(Iₖ) Predicate True if validation of milestone Iₖ is successful CDD initiate_workflow(Grandparent) Function / Operation Starts the TLE workflow for a given grandparent unit (loads context, registers processing unit) TLE LOAD(Grandparent) Operation Atomic load of grandparent data and metadata into TLE context TLE resolve_hierarchy() Function / Operation Internal resolution that computes parent/child relationships and prepares traversal order TLE evaluate_children(Parent) Predicate / Operation Iteratively evaluates each child of Parent for processing eligibility (reads child state, bitmask tests) TLE READ(Parent, Child) Operation Read access to Parent and Child data (used during evaluate_children) TLE update_required(Parent, Child) Predicate True iff a child/parent pair requires an update (e.g., bitmask change or state change) TLE apply_update(Parent, Child, State) Operation Apply the computed update to Parent/Child in-memory state (pre-commit) TLE persist_changes() Operation Flush pending updates to durable storage (pre-commit stage) TLE WRITE(Parent, Child, State) Operation Durable write of Parent/Child state (used when persisting updates) TLE 71 of 186 Term Type Description Methodologies COMMIT(Grandparent) Operation Commit the grandparent-level changes (atomic commit of bitmask / selection) TLE has_next_unit() Predicate True if there is another TLE processing unit (grandparent) to process in the workload TLE has_unprocessed_unit() Predicate True if there exists at least one grandparent unit not yet processed TLE finalize_process() Operation Finalize the overall TLE workflow (cleanup, release resources, produce summary) TLE Table A.1.6. State Machine Identifiers (Used in Tables and Diagrams) State ID Global Label Description Methodologies Using This State S₀ Initialization The initial state, involving loading foundational structures (e.g., DAGs, trees, or graphs) and initializing necessary parameters, queues, or dependency structures All (DAD, DFD, BFD, CDD, PDFD, PBFD, TLE) S₁ Active Processing Represents the core development or processing phase where active work is performed on nodes, levels, or components (e.g., enqueuing, pushing, resolving patterns) DAD, DFD, BFD, CDD S₁(i) Current Pattern/Level Indicates active processing of nodes within Patternᵢ or level i PDFD, PBFD S₁(i+1 ) Next Level/Pattern Progression Processing of Patternᵢ₊₁ or level i+1, typically derived from children of Patternᵢ or level i PDFD, PBFD S₁(j) Refinement Level Reprocessing Patternⱼ or level j due to a validation failure detected in a later stage PDFD, PBFD S₁ (TLE) Parent Batch Loaded Indicates the parent node batch has been loaded and is ready for context-aware evaluation TLE S₂ General Validation / Dependency Check/Refinement A non-parameterized validation phase. Examples include verifying dependency completeness (DAD), backtracking to a parent node (DFD), validating an entire level (BFD), or refining nodes and levels (CDD) DAD, DFD, BFD, CDD S₂(i) Pattern/Level Validation Validates the processed nodes within Patternᵢ or level i PDFD, PBFD S₂(j) Refinement Validation Validates the reprocessed nodes in Patternⱼ or level j during an active refinement cycle PDFD, PBFD S₂ (TLE) Context Established Resolves grandparent-level context to support child node resolution and bitmask evaluation TLE S₃ Graph Extension / Validation General adaptation including node/edge addition and iterative design validation DAD, DFD, CDD S₃(i) Depth-Oriented Process / Resolution Bottom-up subtree validation and subtree resolution before descent PDFD, PBFD S₃(j) Refinement Depth-Oriented Resolution Refinement Depth Resolution - Load required data and resolve node implementation for Patternⱼ during refinement before descending or returning to the original context PBFD S₃ (TLE) Ancestor Data Prepared Loads ancestor-level metadata to support bitmask-based child node resolution TLE S₄ Completion Phase A top-down traversal phase used to finalize unprocessed nodes or patterns, ensuring full coverage and correctness prior to termination PDFD, PBFD 72 of 186 State ID Global Label Description Methodologies Using This State S₄(i) Level / Pattern Completion Phase Completes all unprocessed nodes within Patternᵢ or level i during topdown finalization PDFD, PBFD S₄ (TLE) Children Evaluated Child Node Evaluation via Bitmask Logic – Determines structural inclusion or filtering TLE S₅ Error / Failure Termination Triggered when validation or refinement fails irrecoverably, or Rₘₐₓ (maximum refinement attempts) is exceeded PDFD, PBFD S₅ (TLE) Bitmask Committed Ancestor-Level Bitmask Update – Writes finalized selection to ancestor or top-level structure TLE S₆ (TLE) Traversal Finalized Indicates that the traversal is complete and no further node evaluation remains for the current resolution pass. TLE T Termination The successful conclusion of all phases: all nodes, patterns, and components are validated and finalized. Applies to both flat and hierarchical methods, including hybrid workflows (PBFD, PDFD). All (DAD, DFD, BFD, CDD, PDFD, PBFD, TLE) Table A.1.7. Core CSP Operators Used in DAD, DFD, BFD, CDD, PBFD, PDFD, and TLE Formal Specifications This notation glossary corresponds to the CSPM models verified under FDR 4.2.7 (full specifications hosted in the project’s GitHub repository). Symbol Meaning -> Action Prefix / Event Sequencing: Defines sequential event occurrences where event a occurs then process P executes (Example: a -> P) [] External Choice: Allows environment selection between processes where either A or B can occur based on external input (Example: (event1 -> P1) [] (event2 -> P2)) ; Process Sequencing: Ensures process P completes (reaches SKIP) before process Q begins (Example: P ; Q) SKIP Successful Termination: Represents successful completion of an event or process ? Input Parameter: Receives input from the environment for parameterized events (Example: ?node) ! Output Parameter: Sends output to the environment for parameterized events (Example: !result) [] x:S @ P Indexed External Choice: Enables non-deterministic selection where the environment chooses any element from set S to initiate process P (Example: [] c:NodeID @ process_c) STOP Deadlock / Halt: Represents a blocked state where no events are possible ?x / !x Channel Input / Output: Receives values via ?x or sends values via !x if ... then ... else ... Conditional Branching: Enables guard-based process selection let ... within ... Local Variable Assignment: Defines local variables for intermediate computation RUN(A) Infinite Acceptance: Accepts any event from alphabet A indefinitely [T= P] Trace Refinement: Verifies that process behavior conforms to specification P \ Hiding: Makes specified events internal and unobservable [| X |] Synchronized Parallel Composition: Executes two processes in parallel with required synchronization on events in set X while allowing independent execution of events outside X |~| Internal Non-deterministic Choice: Enables system-internal selection among multiple options without environment influence ||| Interleaving / Independent Parallel: Executes processes independently without event synchronization 73 of 186 Table A.1.8 Three-Level Encapsulation (TLE) Notation This table defines the core notation for the bitmask-based hierarchical data model. Symbol Meaning n Number of root entities (grandparent units) 𝑛𝑚𝑎𝑥 Maximum number of children for any parent entity c_id Identifier of a specific child within a parent bitmask; used for bitwise indexing 𝑃𝑖 Variable number of parent entities for grandparent unit i 𝑃𝑡𝑜𝑡𝑎𝑙 Total number of parent entities across all grandparents 𝑇𝑞𝑢𝑒𝑟𝑦 Time complexity of a single lookup query (Theorem A.10.2) 𝑇𝑢𝑝𝑑𝑎𝑡𝑒 Time complexity of a single update operation (Theorem A.10.3) 𝑇𝑏𝑎𝑡𝑐ℎ Total time complexity of processing all relationships (Theorem A.10.4) 𝐶𝑗 Variable bitmask size in bits for a parent entity j (e.g., 8, 16, 32, 64, or varchar(n)) k Bit length of a traditional foreign key used in the baseline relational representation m Total number of child relationships in the hierarchy ĉ The average number of children per parent across all parent entities Ć The average bitmask size (in bits) across all parent entities w Machine word size used for bitmask storage (e.g., 64 for BIGINT) 𝑆𝑇𝐿𝐸 Total storage size (in bits) required by the TLE model 𝑆𝑡𝑟𝑎𝑑𝑖𝑡𝑖𝑜𝑛𝑎𝑙 Total storage size (in bits) required by the traditional foreign key representation Grandparent Root-level entity that encapsulates multiple parent entities and their hierarchical context Parent Intermediate entity that manages child relationships through bitmask-based selection Child Leaf-level entity evaluated for inclusion/exclusion via parent's bitmask logic A.2 DAD Mermaid Code, Algorithm, and Process Algebra Appendix A.2 provides the formal specification for the Directed Acyclic Development (DAD) methodology, covering its Mermaid diagrams, pseudocode, and CSP model. A.2.1 Structural Workflow Mermaid Code graph TD N1[Node1 Root]-->|Dependency|N2[Node2]; N1-->|Dependency|N3[Node3] N2-->|Dependency|N4[Node4]; N3-->|Dependency|N4 N4-->|Dependency|N5[Node5] legend["DAD Principles:<br>- Acyclicity<br>- Hierarchy<br>- Scalability"]; legendCore[Core]:::core; legendExtended[Extended]:::extended classDef core fill:#E1F5FE,stroke:#039BE5; classDef extended fill:#F0F4C3,stroke:#AFB42B; classDef legend fill:#FFFFFF,stroke:#BDBDBD class N1,N2,N3,N4 core; class N5 extended; class legend legend A.2.2 State Machine Mermaid Code stateDiagram-v2 direction TB [*] --> S₀: DA1 - Load DAG S₀ --> S₁: DAG Validated S₁ --> S₂: DA2 - Validate Dependencies S₂ --> S₁: DA3 - Dependencies Satisfied S₂ --> S₃: DA4 - Missing Dependencies S₃ --> S₁: DA5 - Extension Complete S₁ --> T: DA6 - All Nodes Processed 80 of 186 function no_more_backtrack_points_above(node): // Returns true if there are no remaining ancestors or nodes on stack to process, // indicating the overall traversal is not yet complete. End Procedure A.3.4 CSP Implementation and Formal Verification The complete CSP model (CSPM syntax, FDR 4.2.7 compatible) implementing all operations from Algorithm A.3.3 and state transitions from Table 11 and Table 12 is available in our supplementary repository. Verification Status: All 8 formal properties verified (deadlock-free, divergence-free, deterministic, correct sequencing for DF2-DF7) Repository Access: • GitHub: https://github.com/IBM-Consulting-Formal-Methods/DFD_CSP (commit: b421b32) The model includes all processes (S0-S3, PushChildren) and events documented in Tables A.3.1-A.3.2. See repository README for verification instructions. A.3.5 DFD (Depth-First Development) Methodology Tables The DFD methodology's formal specification is further detailed through Table A.3.1, which provides a unified set of definitions for both the pseudocode and CSP models. Table A.3.2 then outlines the core CSP process algebra, detailing the state transitions and key events that correspond to the pseudocode. Table A.3.1 DFD Methodology - Unified Definitions (Pseudocode + CSP) Pseudocode Term Type Description Pseudocode Lines CSP Mapping Initialization LoadProject(T) Function Initializes tree structure 1 load_tree_actual!t_initial stack ← [C₁] Function Initializes DFS stack 2 initialize_stack_actual!c_root Node Processing Loop stack is not empty Condition Loop continuation 4 stack_not_empty!c stack is empty Condition Termination check 4 stack_is_empty C ← pop(stack) Function Pops node from stack 4a dequeue_actual!c Process(C) Function Core processing 4b dequeue_actual!c Add C to Processed Operation Mark node as processed 4c Tracked in processed set parameter Non-Leaf Processing C is a non-leaf Condition Node has children 4d is_non_leaf!c push(reverse(children(C)), stack) Function Push children for DFS traversal 4e process_child_actual!c → push_children_actual!c → PushChildren process Leaf Processing & Backtracking C is a leaf Condition Node is leaf 4f is_leaf!c Bⱼ ← parent(C) Function Set backtrack point to parent 4g set_backtrack_point_actual!parent(c) Bⱼ is not null Condition Backtracking loop continuation 4h Implicit in S2/S3 recursion has_unprocessed_sibling(Bⱼ) Condition Check for unprocessed siblings 4i has_unprocessed_sibling!b_j 81 of 186 Pseudocode Term Type Description Pseudocode Lines CSP Mapping push(get_unprocessed_sibling(Bⱼ), stack) Function Push sibling to stack 4j get_unprocessed_sibling_actual!b_j → push_sibling_actual!sibling no alternative siblings at Bⱼ Condition No unprocessed siblings remain 4l no_unprocessed_sibling!b_j ValidateSubtree(Bⱼ) Function Subtree validation 4m validate_subtree_actual.Bⱼ Termination Checks stack is empty and no_more_backtrack_points_above(Bⱼ) Condition Final termination check 4n no_more_backtrack_points_above!b_j Terminate() Function Final termination 4o, 5 terminate_successfully_actual Bⱼ ← parent(Bⱼ) Function Backtrack upward to parent 4r backtrack_to_actual!b_j!parent(b_j) Table A.3.2. DFD Methodology - CSP Process Algebra Core (States + Transitions) CSP Process Key Transitions Pseudocode Lines CSP Events S0 (Initialization) DF1: →S1 (Load tree & initialize stack) 1-2 load_tree_actual!t_initial, initialize_stack_actual!c_root S1 (Vertical Processing) DF7: →T (Stack empty termination) 4,5 stack_is_empty, terminate_successfully_actual DF2: →S1 (Non-leaf processing) 4a-4e stack_not_empty!c, dequeue_actual!c, process_actual!c, is_non_leaf!c, process_child_actual!c, push_children_actual!c, PushChildren process (iterates over children) DF3: →S2 (Leaf processing) 4a-4g stack_not_empty!c, dequeue_actual!c, process_actual!c, is_leaf!c, set_backtrack_point_actual!parent(c) S2(Bⱼ) (Backtracking) DF4: →S1 (Process unprocessed sibling) 4h-4j has_unprocessed_sibling!b_j, get_unprocessed_sibling_actual!b_j, push_sibling_actual!sibling DF5: →S3 (No siblings, validate subtree) 4h, 4l-4m no_unprocessed_sibling!b_j, validate_subtree_actual!b_j S3(Bⱼ) (Validation) DF7: →T (Terminate at root) 4n-4o no_more_backtrack_points_above.Bⱼ, terminate_successfully_actual DF6: →S2 (Continue backtracking upward) 4q-4r subtree_validated.Bⱼ, backtrack_to_actual.parent(Bⱼ) T (Termination) Final state 5 terminate_successfully_actual A.3.6 Formal Verification Details for DFD Model and Guarantees All verification checks were performed using FDR 4.2.7 with standard configuration: • Compression: default behavioral reduction (e.g., diamond elimination, sbisim) • Search order: Breadth-first exploration (default, ensures shortest counterexample discovery) The model state space was fully explored. Verification confirms tractability and correctness for all eight critical assertions. Assertions 1–8 • Core safety and liveness (Assertions 1–3): Confirm predictable, non-blocking traversal 82 of 186 • Local processing and control flow (Assertions 4–6, 8): Enforce strict adherence to stack-based sequencing (DF2→DF3) • Validation and termination (Assertion 7): Guarantee that traversal and validation complete before halting A.4 BFD Mermaid Code, Algorithm, and Process Algebra Appendix A.4 provides the formal specification for the Breadth-First Development (BFD) methodology, covering its Mermaid diagrams, pseudocode, and CSP model. A.4.1 Structural Workflow Mermaid Code graph TD A[Level 1: Root] --> B[Level 2: Node 1] A --> C[Level 2: Node 2] A --> D[Level 2: Node 3] B --> E[Level 3: Node 1.1] B --> F[Level 3: Node 1.2] C --> G[Level 3: Node 2.1] D --> H[Level 3: Node 3.1] %% Legend components legendProcessed[Processed]:::processed legendCurrent[Current]:::current legendPending[Pending]:::pending %% Traversal Order classDef processed fill:#99f,stroke:#333 classDef current fill:#9f9,stroke:#333 classDef pending fill:#fff,stroke:#333 %% Apply styling to nodes class A processed class B,C,D current class E,F,G,H pending %% Style edges linkStyle 0,1,2 stroke:#9f9,stroke-width:2px A.4.2 State Machine Mermaid Code stateDiagram-v2 [*] --> S₀ : Initialization S₀ --> S₁ : BF1<br>Graph loaded<br>Initialize level queues with root S₁ --> S₁ : BF2<br>Qₖ ≠ ∅<br>Process node & enqueue children S₁ --> S₂ : BF3<br>∀c ∈ Nₖ - processed(c)<br>Validate level k S₂ --> S₁ : BF4<br>k < L<br>Advance to level k+1 S₂ --> [*] : BF5<br>k = L<br>Terminate A.4.3 Algorithm (Pseudo Code) Algorithm BFD Procedure BFD(T: Tree) Input: T, a hierarchical tree with root node C₁ Output: Level-synchronized implementation // State S₀: Initialization (Table 18) 83 of 186 // Transition BF1: S₀ → S₁ (Table 19) 1. LoadProject(T) // Initialize project and tree structure 2. level_queues ← [[C₁]] // Initialize list of level queues 3. k ← 0 // Initialize current level index 4. Processed ← ∅ // Set to track processed nodes // State S₁: Level Processing (Table 18) - Main BFD loop 5. while k < len(level_queues): 6. Qₖ ← level_queues[k] // Get queue for current level k 7. while Qₖ is not empty: // Transition BF2: S₁ → S₁ (Table 19) - Process nodes at level k 7a. C ← Dequeue(Qₖ) 7b. Process(C) // Core processing action 7c. Add C to Processed // Enqueue children for next level 7d. for each child in children(C): 7e. if len(level_queues) ≤ k+1: 7f. level_queues.append(new_queue()) 7g. enqueue(child, level_queues[k+1]) // Transition BF3: S₁ → S₂ (Table 19) - Current level fully processed 8. ValidateLevel(k) // Validate all nodes at level k // State S₂: Validation (Table 18) - Decide next step after validation 9. if k+1 < len(level_queues): // Transition BF4: S₂ → S₁ (Table 19) - Advance to next level 9a. k ← k + 1 10. else: // Transition BF5: S₂ → T (Table 19) - All levels processed 10a. Terminate() 10b. return // --- Helper Functions --- function ValidateLevel(k): // Validates all nodes at level k End Procedure A.4.4 CSP Implementation and Formal Verification The complete CSP model (CSPM syntax, FDR 4.2.7 compatible) implementing all operations from Algorithm A.4.3 and state transitions from Table 18 and Table 19 is available in our supplementary repository. Verification Status: All formal properties verified (deadlock-free, divergence-free, deterministic, correct sequencing for BF1-BF5 transitions, and behavioral specifications including DequeueImpliesProcess, ValidateBeforeAdvance, and TerminationAtEnd) Repository Access: • GitHub: https://github.com/IBM-Consulting-Formal-Methods/BFD_CSP (commit: 2dd71de) The model includes all processes (S0, S1, S2, T, EnqueueChildSeq) and events documented in Tables A.4.1-A.4.2. See repository README for verification instructions and complete FDR 4.2.7 assertion results. 84 of 186 A.4.5 BFD (Breadth-First Development) Methodology Tables The BFD methodology's formal specification is further detailed through Table A.4.1, which provides a unified set of definitions for both the pseudocode and CSP models. Table A.4.2 then outlines the core CSP process algebra, detailing the state transitions and key events that correspond to the pseudocode. Table A.4.1. BFD Methodology - Unified Definitions (Pseudocode + CSP) Pseudocode Term Type Description Pseudocode Lines CSP Mapping Initialization LoadProject(T) Function Initializes tree structure 1 load_tree_actual!t_initial level_queues ← [[C₁]] Function Initializes level queue structure 2 initialize_level_queues_actual!c_root k ← 0 Variable Current level index 3 (tracked implicitly in S1 parameter lv) Level Processing k < len(level_queues) Condition Check whether more levels remain 5 get_level_queue_actual!k Qₖ is not empty Condition Nodes available at current level k 7 level_queue_not_empty!k Qₖ is empty Condition Current level finished — trigger validation 7 level_queue_empty!k Node Operations C ← Dequeue(Qₖ) Function Dequeues node from level k 7a dequeue_actual!k!C Process(C) Function Perform core processing action for node C 7b process_actual!C Add C to Processed Operation Mark node C as processed for validation/ordering 7c tracked in processed parameter of S1/S2 for each child in children(C) → enqueue(child, level_queues[k+1]) Function Add C's children to next level queue (create next queue if needed) 7d–7g append_new_queue_actual!(k+1) (if needed) then enqueue_child_actual!(k+1)!child for each child Validation & Level Transition ValidateLevel(k) Function Validate all nodes at level k; enter S2 (Validation) 8 validate_level_actual!k → (S2 entry) → level_validated!k k ← k + 1 Operation Advance to next level after successful validation 9a level_validated!k → advance_level_actual!k Termination k + 1 < len(level_queues) Condition Check for next level existence (Advance case) 9 level_validated!k → advance_level_actual!k k + 1 ≥ len(level_queues) / no_more_levels Condition No further levels — final termination case 10 level_validated!k → no_more_levels!k Terminate() Function Final termination of the algorithm 10a, 10b terminate_successfully_actual 85 of 186 Table A.4.2. BFD Methodology - CSP Process Algebra Core (States + Transitions) CSP Process Key Transitions Pseudocode Lines CSP Events S0 BF1: →S1 1-4 load_tree_actual!t_initial, initial-ize_level_queues_actual!c_root S1(k) BF2: →S1 (process node) 7a-7g get_level_queue_actual!k, level_queue_not_empty!k, dequeue_actual!k!C, process_actual!C, [append_new_queue_actual!(k+1)]?, enqueue_child_actual!(k+1)!child* — * means repeated per child; ? means conditional append if next level not present BF3: →S2 (Enter validation) 7, 8 get_level_queue_actual!k, level_queue_empty!k, validate_level_actual!k (enters S2; validation result is emitted from S2 as level_validated!k) S2(k) BF4: →S1 (advance level) 9, 9a level_validated!k, advance_level_actual!k — then continue at S1(k+1) BF5: →T (terminate) 10, 10a level_validated!k, no_more_levels!k, termi-nate_successfully_actual T — final terminate_successfully_actual A.4.6 Formal Verification Details for BFD Model and Guarantees All verification checks were performed using FDR 4.2.7 with standard configuration: • Compression: Default behavioral reduction (e.g., diamond elimination, sbisim) • Search order: Breadth-first state exploration The model state space—tracking six nodes across four levels—was exhaustively explored. Verification confirms tractability and correctness for all eight critical assertions. Assertions 1–8 • Core safety and liveness (Assertions 1–2) guarantee no deadlocks or livelocks. • Determinism (Assertion 3) ensures unique execution paths for any given state. • Dequeue implies process and level validation (Assertions 4–5) ensure correct breadth-first hierarchical processing. • Post-validation behavior and termination correctness (Assertions 6–8) guarantee that BFD completes all levels and nodes. Notes on methodology The breadth-first model assumes no external adversarial interference. Correctness under this model implies correctness under any operational scenario. Passing all FDR assertions demonstrates that BFD’s traversal and level-handling logic is sound, bounded, and deterministic. A.5 CDD Mermaid Code, Algorithm, and Process Algebra Appendix A.5 provides the formal specification for the Cyclic Directed Development (CDD) methodology, covering its Mermaid diagrams, pseudocode, and CSP model. A.5.1 Structural Workflow Mermaid Code graph TD A[Initialization] --> B[Develop/Refine Components] B --> C[Validate Increment] C -->|Feedback/Re-work| B C --> D[Final Delivery] style B fill:#f9f,stroke:#333,stroke-width:2px,stroke-dasharray:5 5 style C fill:#9cf,stroke:#333,stroke-width:2px A.5.2 State Machine Mermaid Code 86 of 186 stateDiagram-v2 [*] --> S₀ S₀--> S₁: CD1<br>Graph loaded S₁--> S₁: CD2<br>Node processed S₁--> S₂: CD3a<br>test_failed(Cᵢ) S₁--> S₂: CD3b<br>feedback_triggered(Cᵢ) S₂--> S₁: CD4a<br>refinement_complete(Cᵢ) S₁--> S₃: CD5<br>all_components_written(Iₖ) S₃--> S₂: CD6<br>feedback_received ∨<br>validation_failed S₃--> [*]: CD7<br>all_increments_validated S₂--> [*]: CD4b<br>refinement_failed ∨<br>refinement_count ≥ M S₃--> S₁: CD8<br>validation_successful ∧<br>more_increments A.5.3 Algorithm (Pseudo Code) Algorithm CDD //Refer to Table 25 and Table 26 for the transition rules Procedure CDD(G: Graph, Rₘₐₓ: Integer, L: Integer) Input: G — A directed project graph Input: Rₘₐₓ— Maximum allowed refinements per component Input: L — Total number of milestones Output: Successfully deployed system, or error // State S₀: Initialization 1. LoadGraph(G) 2. InitializeDependencies(G) 3. current_milestone ← 1 4. refinement_counts ← empty_map() 5. SystemState ← S₁ // Main Loop 6. while SystemState ≠ T: // State S₁: Node Processing 6a. if SystemState = S₁: 6b. if all_components_written(current_milestone) then // Transition CD5: S₁ → S₃ 6c. SystemState ← S₃ 6d. else: // Transition CD2: S₁ → S₁ 6e. C ← SelectAndProcessNode(current_milestone) 6f. Process(C) 6g. Mark C as processed // Transition CD3a, CD3b: S₁ → S₂ 6h. if test_failed(C) or feedback_triggered(C) then 6i. ComponentToRefine ← C 6j. SystemState ← S₂ // State S₂: Refinement 6k. else if SystemState = S₂: 6l. if refinement_counts[ComponentToRefine] ≥ Rₘₐₓ then // Transition CD4b: S₂ → T 6m. TerminateWithError(ComponentToRefine) 6n. else: 87 of 186 6o. refinement_counts[ComponentToRefine] += 1 6p. RefineComponent(ComponentToRefine) 6q. if refinement_successful(ComponentToRefine) then // Transition CD4a: S₂ → S₁ 6r. SystemState ← S₁ 6s. else: // Transition CD4b: S₂ → T 6t. TerminateWithError(ComponentToRefine) // State S₃: Validation 6u. else if SystemState = S₃: 6v. ValidateIncrement(current_milestone) 6w. if validation_failed or feedback_received then // Transition CD6: S₃ → S₂ 6x. ComponentToRefine ← IdentifyFlaw() 6y. SystemState ← S₂ 6z. else: 6aa. if current_milestone < L then // Transition CD8: S₃ → S₁ 6ab. current_milestone += 1 6ac. SystemState ← S₁ 6ad. else: // Transition CD7: S₃ → T 6ae. TerminateSuccess() Procedure TerminateSuccess() 7. SystemState ← T End Procedure Procedure TerminateWithError(C: NodeID) 8. SystemState ← T End Procedure End Procedure A.5.4 CSP Implementation and Formal Verification The complete CSP model (CSPM syntax, FDR 4.2.7 compatible) implementing all operations from Algorithm A.5.3 and state transitions from Table 25 and Table 26 is available in our supplementary repository. Verification Status: All formal properties verified (deadlock-free, divergence-free, deterministic, correct sequencing for CD1-CD8 transitions, dependency respect verification for N4 and N5, bounded refinement with Rmax enforcement, and hostile environment verification for worst-case refinement scenarios) Repository Access: • GitHub: https://github.com/IBM-Consulting-Formal-Methods/CDD_CSP (commit: 03b972d) The model includes all processes (S0, S1, S2, S3) and events documented in Tables A.5.1-A.5.2, featuring actual dependency graph modeling with parallel processing capabilities and bounded refinement loops. See repository README for verification instructions and complete FDR 4.2.7 assertion results including dependency compliance proofs and refinement bound verification. A.5.5 CDD (Cyclic Directed Development) Methodology Tables The CDD methodology's formal specification is further detailed through Table A.5.1, which provides a unified set of definitions for both the pseudocode and CSP models. Table 88 of 186 A.5.2 then outlines the core CSP process algebra, detailing the state transitions and key events that correspond to the pseudocode. Table A.5.1. CDD Methodology - Unified Definitions (Pseudocode + CSP) Pseudocode Term Type Description Pseudocode Lines CSP Mapping Initialization LoadGraph(G) Function Loads project graph 1 load_graph_actual!Graph InitializeDependencies() Function Initializes dependencies 2 initialize_dependencies_actual current_milestone ← 1 Variable Set initial milestone 3 (Implied in S1(M1) parameter) Internal State refinement_counts Variable Tracks refinement attempts (parameter attempts in S2) 4, 6o (Abstracted as attempts parameter in S2) Component Processing SelectAndProcessNode() Function Node processing action 6e-6f process_node_actual!NodeID test_failed(C) Condition Test failure → S2 (CD3a) 6h test_failed_actual!NodeID feedback_triggered(C) Condition Feedback detected → S2 (CD3b) 6h feed-back_triggered_actual!NodeID all_components_written(k) Condition Milestone complete check 6b all_components_written_actual!MilestoneID Refinement RefineComponent(C) Function Initiates refinement attempt 6p refine_component_actual!NodeID → refine-ment_confirmed_actual!NodeID refine-ment_successful(C) Condition Refinement successful 6q refine-ment_complete_actual!NodeID refinement_failed(C) Condition Refinement failed → check Rmax 6s refinement_failed_actual!NodeID Validation ValidateIncrement(k) Function Validates milestone increment k 6v vali-date_increment_actual!MilestoneID validation_failed Condition Validation failed → S2 (CD6) 6w valida-tion_failed_actual!MilestoneID feedback_received Condition Feedback received after validation → S2 (CD6) 6w feed-back_received_actual!MilestoneID IdentifyFlaw() Function Identifies flawed component 6x identify_flaw_actual?NodeID Termination current_milestone < L Condition Advance to next milestone check 6aa milestone_lt(k, L_max) (Implied in S3 logic) current_milestone += 1 Variable Assignment Increments milestone counter 6ab ad-vance_milestone_actual!Next_Milestone(k) FinalDeployment() Function Final deployment 6ae final_deployment_actual TerminateSuccess() Function Successful termination 7, 6ae final_development_actual → terminate_successfully_actual TerminateWithError() Function Error termination (Rmax exceeded) 8, 6m, 6t termi-nate_with_error_actual!NodeID 89 of 186 Table A.5.2. CDD Methodology - CSP Process Algebra Core (States + Transitions) CSP Process Key Transitions Pseudocode Lines CSP Events S0 CD1: →S1 (Load & init) 1-5 load_graph_actual!Graph, initialize_dependencies_actual S1(k, n1..n5) CD2: →S1 (Process success) 6e-6g process_node_actual!C → mark_completed → S1 self-loop CD3a: →S2 (Test failure) 6h-6j process_node_actual!C → test_failed_actual!C → S2(C, k, n1..n5, 0) CD3b: →S2 (Feedback) 6h-6j process_node_actual!C → feedback_triggered_actual!C → S2(C, k, n1..n5, 0) CD5: →S3 (Milestone complete) 6b-6c all_components_written_actual!k → validate_increment_actual!k → S3(k, n1..n5) S2(c, k, n1..n5, attempts) CD4a: →S1 (Refinement success) 6p-6r refine_component_actual!c → refinement_confirmed_actual!c → refinement_complete_actual!c → S1(k, n1..n5) CD4b: → S0 (Error termination with S0 instead of T for FDR liveness verification) 6m, 6t refine_component_actual!c → refinement_confirmed_actual!c → refinement_failed_actual!c → [Rmax check] → terminate_with_error_actual!c → S0 S3(k, n1..n5) CD6: →S2 (Validation failure) 6w-6y (validation_failed_actual!k → identify_flaw_actual?c → mark_not_completed) □ (feedback_received_actual!k → identify_flaw_actual?c → mark_not_completed) → S2(c, k, n1..n5, 0) CD8: →S1 (Advance milestone) 6z-6ac milestone_lt(k, L_max) → advance_milestone_actual!Next_Milestone(k) → S1(Next_Milestone(k), NotCompleted, ...) CD7: → 0 (Final success) 6ad-6ae ¬ milestone_lt(k, L_max) → final_development_actual → terminate_successfully_actual → S0 T Termination final Not explicitly used as a final state; replaced by → S0 for liveness verification. A.5.6 Formal Verification Details for CDD Model and Guarantees All verification checks were performed using FDR 4.2.7 with standard configuration: • Compression: Default behavioral reduction (e.g., diamond elimination, sbisim) • Search order: Breadth-first state exploration The model state space—tracking five nodes across three milestones plus the refinement counter—was exhaustively explored. The cumulative verification demonstrates tractability for all 10 assertions. Dependency respect verification (Assertions 6 & 7) • N4 (Assertion 6): Verified that N4 cannot execute until both N2 and N3 complete. Trace refinement confirms all observable behaviors respect this dependency. • N5 (Assertion 7): Verified that N5 cannot execute until N4 completes. Trace refinement confirms strict sequential enforcement. Refinement bound verification (Assertions 8 & 9) • Using the Hostile Environment technique, the system is exposed to persistent refinement failures: o Always triggers validation_failed_actual o Always triggers refinement_failed_actual • Passing deadlock and divergence checks confirms: o Maximum Rₘₐₓ attempts are enforced. o System terminates with terminate_with_error_actual. o Infinite refinement loops are prevented. 96 of 186 Pseudocode Term Type Description Pseudocode Lines CSP Mapping else: call S4_TopDownCompletion(L1) State Transition Transitions to the Top-Down Completion state (PD5). 84-86 S4_TopDownCompletion(L1) S₄: Top-Down Completion Finalize_Unprocessed_Nodes(i) Procedure Finalizes and validates any remaining unprocessed nodes. 99 finalize_unprocessed!i if i != L5: call S4_TopDownCompletion(Next(i)) State Transition Continues top-down to the next level (PD6). 103-105 S4_TopDownCompletion(Next(i)) else: call T State Transition Transitions to the successful termination state (PD7). 106-108 T if Trace_Origin_Exists(i) Condition Checks if refinement is possible after failure (PD6a). 111 cond_trace_origin_exi sts?i else: call S5 State Transition Transitions to the terminal error state (PD6b). 121-122 cond_trace_origin_no t_exists?i → S5 Final Outcome call T Termination The system terminates successfully. 125-126 terminate_success → T call S5 Termination The system terminates with an error. 129-130 terminate_error → S5 Table A.6.2 PDFD Methodology - CSP Process Algebra Core (States + Transitions) CSP Process Key Transitions Pseudocode Lines CSP Events (Simplified) S₀ PD1: Initial start 1–6 process_level!L1 → S1_InitialProcess(L1) S₁_InitialProcess(i) PD2: Core sequence start 9–14 process_level!i → S2_LevelValidation(i) PD8: Exhaustion check 11 cond_refinement_exhausted?i → S5 S₁_RefinementProcess(j, i_orig) PD3: Core sequence start 20–25 process_level!j → S2_RefinementValidation(j, i_orig) PD8: Exhaustion check 22 cond_refinement_exhausted?j → S5 S₂_RefinementValidation(j, i_orig) PD3 (Entry) 53–54 validate_level!j → ... PD3a/PD3b: Refinement success 56–64 cond_threshold_met?j → S3_RefinementResolution(...) PD3c: Refinement failure 66–73 cond_threshold_not_met?j → (refinement choice) S₃_RefinementResolution(j, i_orig) PD3a: Continue deep refinement 58–61 cond_j_lt_i.j.i_orig -> S1_RefinementProcess PD3b: Resume validation context 62–64 cond_j_lt_i.j.i_orig → S1_RefinementProcess(Next(j), i_orig) S₂_LevelValidation(i) PD2b: Advance level 39–40 cond_threshold_met?i → S1_InitialProcess(Next(i)) PD4: Go bottom-up (mandatory) 48–50 cond_has_no_children?i → S3_BottomUpCompletion(i) PD2a: Refine (failure path) 44–47 cond_refinement_available?j → increment_attempts!j → S1_RefinementProcess(j, i) S₃_BottomUpCompletion(i) PD4a: Move up 80–83 finalize_subtrees!i → cond_all_descendants_validated?i → S3_BottomUpCompletion(Prev(i)) 97 of 186 CSP Process Key Transitions Pseudocode Lines CSP Events (Simplified) PD5: Start top-down 84–86 finalize_subtrees!i → cond_all_descendants_validated?i → S4_TopDownCompletion(L1) PD4b: Refine (failure) 88–95 cond_not_all_descendants_validated?i → SimpleRefinementHandler(i) S₄_TopDownCompletion(i) PD6: Move down 102–105 finalize_unprocessed!i → cond_all_descendants_validated?i → S4_TopDownCompletion(Next(i)) PD7: Success 106–108 finalize_unprocessed!i → cond_all_descendants_validated?i → T PD6a: Refine (failure) 110–119 cond_not_all_descendants_validated?i → cond_trace_origin_exists?i → SimpleRefinementHandler(i) PD6b: Error 120–122 cond_not_all_descendants_validated?i → cond_trace_origin_not_exists?i → S5 S₅ / T Termination 125–130 terminate_error → S5 / terminate_success → T A.6.6 Formal Verification Details for PDFD Model and Guarantees All verifications were performed in FDR 4.2.7 using default behavioral reduction (e.g., sbisim, diamond elimination) and breadth-first exploration. Scope The model tracks: • Five core levels (L1–L5) • Core and refinement transitions • The refinement attempt counter All 11 assertions completed exhaustively within this state space. 1. Structural Integrity (1 Assertion) Determinism System :[deterministic [F]] confirms the system’s progression is fully driven by conditional events offered by CondEnv, with no implicit nondeterminism. 2. Consistency and Soundness (6 Assertions) Mutual Exclusivity All conditional decision pairs (cond_X) were proven disjoint. Example: ConditionConsistency_ThresholdMet [T= STOP] guarantees cond_threshold_met and cond_threshold_not_met cannot both be enabled. This validates the soundness of the transition rules at every decision point. 3. Liveness and Bounded Termination (4 Assertions) Deadlock-, Livelock-, and Divergence-Free These checks confirm that termination is always reached safely and that bounded refinement is enforced without hidden cycles. Protocol View Confirmation SystemProtocolView :[divergence free] confirms that correctness is preserved even when conditional events are abstracted. A.7 PBFD Mermaid Code, Algorithm, and Process Algebra Appendix A.7 provides the formal specification for the Primary Breadth-First Development (PBFD) methodology, covering its Mermaid diagrams, pseudocode, and CSP model. A.7.1 Structural Workflow Mermaid Code flowchart TD A0([Start]) --> A1[Initialize Pattern₁] 98 of 186 A1 --> A2[Process Patternᵢ] %% Proceed if all nodes are validated A2 -->|All nodes validated| A3[Proceed to next level Patternᵢ₊₁] A2 -->|Validation failed| A4[Backtrack to Patternⱼ] %% j is determined by trace_origin(i) A4 -->|refinement_attemptsⱼ < Rₘₐₓ| A2 A4 -->|refinement_attemptsⱼ >= Rₘₐₓ| A5[Error: Exhausted Rₘₐₓ] A3 -->|i < L ∧ Patternᵢ₊₁ != ∅| A2 A3 -->|i < L ∧ Patternᵢ₊₁ = ∅| A6[Start Top-Down Finalization] A3 -->|i = L| A6 A6 --> A7[Finalize Patternᵢ] A7 -->|All nodes processed| A8[Advance to Patternᵢ₊₁] A8 -->|i < L| A7 A8 -->|i = L| A9([Done]) A.7.2 State Machine Mermaid Code stateDiagram-v2 %% ──────────────── Initialization Phase ──────────────── state "S0: Entry Point" as S0_init %% ──────────────── Progression Phase ──────────────── state "S1(i): Current Pattern Processing" as S1_i state "S1(i+1): Next Pattern (Children)" as S1_i_plus_1 state "S2(i): Pattern Validation" as S2_i state "S3(i): Depth Resolution" as S3_i %% ──────────────── Refinement Phase ──────────────── state "S1(j): Refinement Level Processing" as S1_j state "S1(j+1): Refinement Progression" as S1_j_plus_1 state "S2(j): Refinement Validation" as S2_j state "S3(j): Refinement Depth Resolution" as S3_j %% ──────────────── Completion Phase ──────────────── state "S4(1): Completion Phase Entry" as S4_1_entry state "S4(i): Completion Level" as S4_i state "S4(L): Last Completion Level" as S4_L %% ──────────────── Terminal States ──────────────── state "S5: Error - Terminate" as S5_error state "T: Terminate" as T_success %% ──────────────── Choice Pseudostates ──────────────── state PB1_ch <<choice>> state PB2_ch <<choice>> state PB3_ch <<choice>> 99 of 186 state PB3a_ch <<choice>> state PB3a_post_ch <<choice>> state PB4a_ch <<choice>> state PB4b_ch <<choice>> state PB5_ch <<choice>> state PB6_ch <<choice>> state PB7_ch <<choice>> %% ──────────────── Initial Flow ──────────────── [*] --> S0_init S0_init --> PB1_ch PB1_ch --> S1_i : PB1 - i = 1 %% ──────────────── Pattern Progression ──────────────── S1_i --> PB2_ch PB2_ch --> S2_i : PB2 - Node unvalidated PB2_ch --> S3_i : PB2a - All validated %% ──────────────── Pattern Validation (S2_i) ──────────────── S2_i --> PB3_ch PB3_ch --> S1_j : PB3 - Backtrack possible PB3_ch --> S3_i : PB4 - All validated PB3_ch --> S5_error : PB3c - No backtrack possible %% ──────────────── Refinement Handling (S1_j to S3_j) ──────────────── S1_j --> PB3a_ch PB3a_ch --> S2_j : PB3a - Node unvalidated PB3a_ch --> S3_j : PB3b - All validated S1_j --> S5_error : PB9 - Attempts exhausted S2_j --> PB3a_post_ch PB3a_post_ch --> S3_j : PB3a1 - All validated PB3a_post_ch --> S1_j : PB3a2 - Retry refinement PB3a_post_ch --> S5_error : PB3a3 - Attempts exhausted %% ──────────────── Post-Refinement Actions (S3_j) ──────────────── S3_j --> PB5_ch PB5_ch --> S1_j_plus_1 : PB5 - Resume next level (j < i) S3_j --> PB6_ch PB6_ch --> S3_i : PB6 - Refinement complete (j = i) %% ──────────────── Descent or Completion Decision (S3_i) ──────────────── S3_i --> PB4a_ch PB4a_ch --> S1_i_plus_1 : PB4a - Recurse to critical children S3_i --> PB4b_ch 100 of 186 PB4b_ch --> S4_1_entry : PB4b - Start Completion %% ──────────────── Completion Phase ──────────────── S4_1_entry --> S4_i S4_i --> PB7_ch PB7_ch --> S4_i : PB7 - Advance (i+1 < L) PB7_ch --> S4_L : PB7 - Advance to Last (i+1 = L) PB7_ch --> S1_j : PB7a - Unfinalized → backtrack PB7_ch --> S5_error : PB7b - Unfinalized → no backtrack S4_L --> T_success : PB8 - All levels completed %% ──────────────── Final Transitions ──────────────── S5_error --> [*] T_success --> [*] A.7.3 Algorithm (Pseudo Code) Algorithm PBFD // ======================== // Structural Helper Functions // ======================== // Table 40, Rule PB3/PB7a: Determines the lowest-level pattern that caused the failure. Function trace_origin(i: Integer, check_predicate: Function) Returns Integer // Find j = min{k | k < i ∧ check_predicate(Patternₖ, Patternᵢ)} // The check_predicate is either 'affected_by' (for PB3) or 'affected_by_unprocessed' (for PB7a). j_list ← {k | k < i ∧ check_predicate(Patternₖ, Patternᵢ)} if j_list is empty then return UNDEFINED // Handles PB3c condition: trace_origin undefined else return min(j_list) End Function // Table 40, Rule PB5: Finds the next level to process within the original refinement scope (j to i_orig). Function determine_next_refinement_level(j: Integer, i_orig: Integer) Returns Integer // In PBFD, refinement is horizontal advancement after a success at j. // The next level is simply j+1, provided j+1 is still within the original scope. if j + 1 <= i_orig then return j + 1 else // This case should be caught by the PB6 condition (j = i_orig) but included for safety. return UNDEFINED End Function // ======================== // Critical Children Selection Procedure // ======================== 101 of 186 Function select_critical_children(available_children: Set[Node], level: Integer) // Selection criteria based on architectural criticality critical_children ← ∅ for each child in available_children do if is_on_critical_path(child) ∨ has_high_fanout(child) ∨ is_foundational_component(child, level) then critical_children ← critical_children ∪ {child} end if end for return critical_children End Function // ======================== // Consolidated Refinement Handler // Covers Table 40: Rules PB3/PB3c and PB7a/PB7b // ======================== Function HandlePBFDFailureRefinement( current_failed_level: Integer, R_MAX: Integer, find_j_predicate: Function ) Returns State // Table 40, Rule PB3/PB7a: Find root cause level (using trace_origin) 1: j ← trace_origin(current_failed_level, find_j_predicate) // Table 40, Rule PB3/PB7a: Check refinement possibility (j defined AND attempts < R_MAX) 2: if j is defined and refinement_attempts[j] < R_MAX then 3: refinement_attempts[j]++ 4: Return S1_RefinementProcess(j, current_failed_level) // → S1(j) via PB3/PB7a // Table 40, Rule PB3c/PB7b: Termination (j undefined OR attempts exhausted) 5: else 6: Return S5 // → S5 via PB3c/PB7b End Function // ======================== // Main PBFD Algorithm // ======================== Procedure PBFD(T: Tree, L: Integer, R_MAX: Integer) Input: Tree T (L levels), Rₘₐₓ Output: Processed tree or error // Table 39: S0 Initialization 1: Load T, initialize refinement_attempts[1..L] = 0 2: i ← 1, currentState ← S1_InitialProcess(i) // Table 40, Rule PB1: → S1(1) 102 of 186 3: while currentState ∉ {T, S5} do 4: case currentState of // Table 39: S1(i) Main Pattern Processing 5: S1_InitialProcess(i): 6: Process Patternᵢ 7: if ∃n ∈ Patternᵢ: ¬validated(n) then // Rule PB2: → S2(i) 8: currentState ← S2_ValidationInitial(i) 9: else if ∀n ∈ Patternᵢ: validated(n) then // Rule PB2a: → S3(i) 10: currentState ← S3_DepthProgression(i) // Table 39: S2(i) Initial Pattern Validation 11: S2_ValidationInitial(i): 12: Validate Patternᵢ // Rule PB4 Action 13: if ∀n ∈ Patternᵢ: validated(n) then // Rule PB4: → S3(i) 14: currentState ← S3_DepthProgression(i) 15: else if ∃n ∈ Patternᵢ: ¬validated(n) then // Rule PB3/PB3c: Refinement or Termination 16: currentState ← HandlePBFDFailureRefinement(i, R_MAX, affected_by) // Table 39: S1(j) Refinement Processing 17: S1_RefinementProcess(j, i_orig): 18: if refinement_attempts[j] ≥ Rₘₐₓ then // Rule PB9: → S5 19: currentState ← S5 20: else 21: Process Patternⱼ 22: if ∃n ∈ Patternⱼ: ¬validated(n) then // Rule PB3a: → S2(j) 23: currentState ← S2_ValidationRefinement(j, i_orig) 24: else if ∀n ∈ Patternⱼ: validated(n) then // Rule PB3b: → S3(j) 25: currentState ← S3_RefinementDepthResolution(j, i_orig) // Table 39: S2(j) Refinement Validation 26: S2_ValidationRefinement(j, i_orig): 27: if ∀n ∈ Patternⱼ: validated(n) then // Rule PB3a1: → S3(j) 28: currentState ← S3_RefinementDepthResolution(j, i_orig) 29: else if ∃n ∈ Patternⱼ: ¬validated(n) and refinement_attempts[j] < Rₘₐₓ then // PB3a2 30: refinement_attempts[j]++ 31: currentState ← S1_RefinementProcess(j, i_orig) // → S1(j) 32: else if ∃n ∈ Patternⱼ: ¬validated(n) and refinement_attempts[j] ≥ Rₘₐₓ then // PB3a3 33: currentState ← S5 // → S5 // Table 39: S3(i) Depth-Oriented Resolution 34: S3_DepthProgression(i): 35: //Implement Pattern Derivation (Table 40, Rule PB4a action); Select critical children for next pattern (not all children) 36: Patternᵢ₊₁ ← ∅ 37: available_children ← {c ∈ V | ∃n ∈ Patternᵢ: (n,c) ∈ E} 38: Patternᵢ₊₁← select_critical_children(available_children, i) 103 of 186 39: if i < L and Patternᵢ₊₁ ≠ ∅ then // Rule PB4a: → S1(i+1) 40: i ← i+1, currentState ← S1_InitialProcess(i) 41: else if i = L or Patternᵢ₊₁ = ∅ then // Rule PB4b: → S4(1) 42: i ← 1, currentState ← S4(i) // Table 39: S3(j) Refinement Depth Resolution 43: S3_RefinementDepthResolution(j, i_orig): 44: if j < i_orig then // Rule PB5: → S1(j+1) 45: next_level ← determine_next_refinement_level(j, i_orig) //Get next level 46: currentState ← S1_RefinementProcess(next_level, i_orig) 47: else if j = i_orig then // Rule PB6: → S3(i_orig) 48: currentState ← S3_DepthProgression(i_orig) // Table 39: S4(i) Completion Phase 49: S4(i): 50: Finalize Patternᵢ 51: if ∀n ∈ Patternᵢ: processed(n) then 52: if i < L then // Rule PB7: → S4(i+1) 53: i ← i+1, currentState ← S4(i) 54: else if i = L then // Rule PB8: → T 55: currentState ← T 56: else if ∃n ∈ Patternᵢ: ¬ processed(n) then 57: currentState ← HandlePBFDFailureRefinement(i, R_MAX, affected_by_unprocessed) // PB7a/PB7b 58: end case 59: end while // Final Termination (Table 40) 60: if currentState = S5 then Terminate with error 61: else if currentState = T then Terminate successfully End Procedure A.7.4 CSP Implementation and Formal Verification The complete CSP model (CSPM syntax, FDR 4.2.7 compatible) implementing all operations of the Primary Breadth-First Development (PBFD) methodology from Algorithm A.7.3 and state transitions from Table 39 and Table 40 —including its breadth-first with S3_DepthProgression logic, state transitions, conditional decision predicates, and R_max bounding mechanism—is available in our supplementary repository. Verification Status: All 33 core formal properties verified successfully: Core Safety & Liveness: Deadlock-free and divergence-free under both normal and hostile conditions State-Level Safety: Successful verification of 26 state-level assertions, covering every operational and terminal state (S0–S5, T) across all level combinations (L1, L2, L3) in both normal and refinement contexts Conditional Soundness: Verified mutual exclusivity of validation conditions, ensuring no contradictory conditional states 104 of 186 Hostile Environment Robustness: Deadlock-free operation under adversarial conditional environments Bounding Guarantee: Verified R_max enforcement, ensuring termination even in failure scenarios. The model includes the main system process (PBFD → System), the conditional environment (LegalCondEnv), the hostile conditional environment (HostileEnv), and all necessary supporting processes for state management. The flow is guaranteed to be bounded by the R_max refinement limit, ensuring safe termination in all worst-case scenarios. Repository Access: • GitHub: https://github.com/IBM-Consulting-Formal-Methods/PBFD_CSP (commit: ea1a3bc) See the repository README for verification instructions and complete FDR 4.2.7 assertion results detailing all 33 passing assertions. A.7.5 PBFD (Primary Breadth-First Development) Methodology Tables The PBFD methodology's formal specification is further detailed through Table A.7.1, which provides a unified set of definitions for both the pseudocode and CSP models. Table A.7.2 then outlines the core CSP process algebra, detailing the state transitions and key events that correspond to the pseudocode. Table A.7.1. PBFD Methodology - Unified Definitions (Pseudocode + CSP) Pseudocode Term Type Description Pseudocode Lines CSP Mapping Initialization Load T System Function Initializes tree structure and pattern hierarchy PBFD: 1 load_tree_actual initialize refinement_attempts System Function Sets all level refinement counters to 0 PBFD: 1 initialize_refinement_attempts_actual currentState ← S1_InitialProcess State Transition Begins main pattern processing (PB1) PBFD: 2 S1_InitialProcess(L1) Pattern Processing Process Patternᵢ Pattern Function Executes core pattern processing (PB2) PBFD: 6 process_pattern_actual.i Validate Patternᵢ Validation Action Performs pattern validation (PB4 Action) PBFD: 12, 27 validate_pattern_actual.i ∃n ∈ Patternᵢ: ¬validated(n) Validation Condition Pattern validation failed (PB2) PBFD: 7, 22, 29, 32 cond_not_all_validated?i ∀n ∈ Patternᵢ: validated(n) Validation Condition Pattern validation succeeded (PB2a, PB4) PBFD: 9, 13, 24, 27 cond_all_validated?i Refinement Control Find j Trace Function Identifies minimal root cause level j (PB3/PB7a) HandlePBFDFailureRefinement: 1 (Implicit in TryTraceOrigin using cond_trace_origin) affected_by_unprocessed Trace Function Finds patterns affecting unprocessed nodes PBFD: 57 (Implicit in TryTraceOrigin_Completion) refinement_attempts[j]++ Counter Operation Increments refinement attempts for level j (PB3/PB3a2/PB7a) HandlePBFDFailureRefinement: 3, PBFD: 30 increment_refinement_attempts_actual.j refinement_attempts[j] ≥ Rₘₐₓ Limit Check True when refinement attempts for level j ≥Rmax (PB3c/PB3a3/PB7b/PB9) HandlePBFDFailureRefinement: 5 (else branch), PBFD: 18, 32 cond_ref_attempts_ge_Rmax?j 105 of 186 Pseudocode Term Type Description Pseudocode Lines CSP Mapping refinement_attempts[j] < Rₘₐₓ Limit Check True when refinement attempts for level j <Rmax (PB3/PB3a2/PB7a) HandlePBFDFailureRefinement: 2, PBFD: 29 cond_ref_attempts_lt_Rmax?j HandlePBFDFailureRefinement Procedure Handles PB3/PB3c/PB7a/PB7b logic PBFD: 16, 57 TryTraceOrigin_Initial/Completion Critical Children Selection available_children(Patternᵢ) Function Returns set of direct child nodes: {c ∈ V | ∃n ∈ Patternᵢ: (n,c) ∈ E} PBFD: 37 (Implied by resolve_depth_actual) is_on_critical_path(c) Predicate True if node c lies on critical path from roots to leaves select_critical_children (Not directly mapped, external logic) has_high_fanout(c) Predicate True if node c has ≥3 dependents select_critical_children (Not directly mapped, external logic) is_foundational_component(c, level) Predicate True if node c provides foundational services for its level select_critical_children (Not directly mapped, external logic) select_critical_children(available_children, level) Procedure Selects architecturally critical nodes for Patternᵢ₊₁ PBFD: 38 select_critical_children_actual.i Depth Processing Patternᵢ₊₁ ≠ ∅ Existence Check True when next level has no pattern entries (PB4b) PBFD: 39 cond_pattern_next_nonempty.i i < L Boundary Check True when not at max level (PB4a/PB7) PBFD: 39, 52 cond_i_lt_L?i i = L Boundary Check True at max level (PB4b/PB8) PBFD: 41, 54 cond_i_eq_L?i Patternᵢ₊₁ = ∅ Existence Check True when next level has patterns (PB4b) PBFD: 41 cond_pattern_next_empty?i Completion Phase Finalize Patternᵢ Completion Function Processes remaining nodes (PB7/PB8) PBFD: 50 finalize_pattern_actual.i processed(n) State Predicate True when node n is fully processed (P(n)=1 ∨ P(n)=2) Implied by PBFD: 51, 56 (Implied by cond_all_processed) ∃n∈Patternᵢ:¬processed(n) Validation Condition Pattern has unprocessed nodes (PB7a/PB7b) PBFD: 56 cond_not_all_processed?i ∀n∈Patternᵢ:processed(n) Validation Condition All nodes processed (PB7/PB8) PBFD: 51 cond_all_processed?i Termination S5 Error State Terminal state for all error conditions (PB3c/PB3a3/PB7b/PB9) PBFD: 60 terminate_failure_actual → S5 T Success State Terminal state for successful completion (PB8) PBFD: 61 terminate_success_actual → T 112 of 186 • k₁ Strict Decrease: PB4a and PB7 finalize nodes, reducing the highest-priority component. • k₂ Strict Decrease: PB3, PB3a2, and PB7a consume refinement attempts and strictly reduce k₂, ensuring lexicographic progress even when backtracking causes k₃ to increase temporarily. • k₃ Decrease Role: The phase-progression transitions PB2, PB2a, PB3a, PB3a1, PB3b, PB4, and PB4b strictly reduce k₃ (phase ordinal), ensuring forward progress through the main execution path. Although k₃ may temporarily increase in commit transition PB4a and refinement/backtracking transitions (PB3, PB3a2, PB7a), the overall lexicographic decrease is guaranteed by the strict reduction of higher-priority components k₁ or k₂. • k₄ Strict Decrease: PB5 and PB6 reduce intra-phase progress when higher-priority components remain unchanged. Terminal rules PB3a3, PB3c, PB7b, PB8, and PB9 end the computation and do not require measure reduction. Since every non-terminal transition strictly decreases M lexicographically, the measure is well-founded and termination is guaranteed. ∎ A.8.2 Lemma (Bounded Refinement) Statement. For all levels k ∈ [1, L]: □(refinement_attempts(k) ≤ R ₘₐₓ ). In any non-terminal state, any active refinement target j satisfies refinement_attempts(j) < R ₘₐₓ . Terminal states S₅ are reached only when an attempt bound is exhausted. Proof. • Base Case. At initial state S₀: ∀k: refinement_attempts(k)=0 ≤ Rₘₐₓ. The statement holds vacuously. • Inductive Step. Assume in state S the invariant holds. Consider a transition S → S′. Only refinement-entry rules increment refinement_attempts(j). From Tables A.8.2 - A.8.3 these are explicitly guarded by refinement_attempts(j) < Rₘₐₓ (PD2a, PD3c, PD4b, PD6a for PDFD; PB3, PB3a2, PB7a for PBFD). Hence any increment preserves refinement_attempts(j) ≤ Rₘₐₓ. All other rules leave all refinement counters unchanged. Terminal rules (e.g., PD6b, PD8, PB3a3, PB9, PB7b, PB3c) fire only when refinement_attempts(j) ≥ Rₘₐₓ for some j. Terminal transitions (which fire only when refinement_attempts(j) ≥ Rₘₐₓ) do not increment counters, preserving the invariant. • Conclusion. By induction on transitions, the counter is bounded by Rₘₐₓ at all times. Since at most L levels can each suffer at most Rₘₐₓ increments, the total number of refinement attempts is bounded by L ⋅ Rₘₐₓ. Thus k₂ is finite and strictly decreases on each refinement entry until exhaustion. ∎ A.8.3. Lemma (Finalization Monotonicity) Statement. Once a node n has been permanently finalized (P(n)=2), it remains finalized unless a refinement backtrack explicitly resets it. Resets occur only on refinement-entry rules and are strictly controlled by attempt bounds. Moreover, across execution, k₁ (the count of unfinalized nodes) is monotone non-increasing except when a controlled reset (paired with a decrease in k₂) occurs. Proof. • Base Case. Initially no node is finalized (P(n) ≠ 2 for all n). The statement holds vacuously in the initial state. • Finalization Step: Per Tables A.8.2 - A.8.3, the rules that set nodes to finalized (i.e., produce committed P(n)=2) are the commit/finalize transitions PDFD: 113 of 186 PD2b and PD6; PBFD: PB4a and PB7). In both algorithms, these transitions strictly reduce k₁. No other transition creates P(n)=2. • Reset rules. The only rules that may reset previously finalized nodes to nonfinalized ones (i.e., potentially Δk₁ > 0) are refinement-entry/backtrack rules (PD2a, PD3c, PD4b, PD6a; PB3, PB3a2, PB7a). Each such rule has the guard refinement_attempts(j) < Rₘₐₓ and the operational semantics of attempting correction. On taking such a rule, k₂ strictly decreases (since refinement_attempts(j) is incremented). No non-refinement rule resets finalized nodes. • Lexicographic compensation. Therefore, any transition that reverses finalization (i.e., a reset that potentially increases k₁) is guaranteed to be a refinemententry transition that strictly decreases k₂. Hence the pair (k₁, k₂) is lexicographically non-increasing across transitions: a rise in k₁ is strictly compensated by a fall in k₂. • Conclusion. k₁ is monotone non-increasing unless a bounded, recorded refinement reset occurs; such resets are bounded by Lemma A.8.2. Thus the finalization invariant holds. ∎ A.8.4 Lemma (Termination Guarantee) Statement. For any finite tree G = (V, E) and finite parameters L, R ₘₐₓ ∈ N⁺, any execution of PDFD or PBFD terminates in either: • Success T: all nodes finalized (∀n ∈ V: P(n) = 2), or • Bounded failure S₅: refinement exhausted for some level (∃j: refinement_attempts(j) = Rₘₐₓ). Proof. • Well-foundedness. Each component of M = (k₁, k₂, k₃, k₄) ranges over a wellfounded (finite or well-ordered) set: o 0 ≤ k₁ ≤ |V|. o 0 ≤ k₂ ≤ L ⋅ Rₘₐₓ. o k₃ ∈ {0, 1, 2, 3, 4}. o k₄ bounded by finite batch sizes (≤|V|). Thus no infinite strictly decreasing sequence in M exists. • Measure descent on transitions. From the exhaustive ΔM annotations in Tables A.8.2A.8.3, every non-terminal transition strictly decreases M in lexicographic order: o If a non-terminal transition finalizes nodes, it decreases k₁. o If it is a refinement-entry, it decreases k₂. o Otherwise the phase/intra-phase components (k₃, k₄) strictly decrease. • No infinite execution sequences. Since M decreases on every non-terminal step and M is well-founded, the system cannot execute infinitely many non-terminal moves. Therefore, every execution sequence reaches a terminal state. • Terminal classification. Terminal rules in Tables A.8.2A.8.3 correspond exactly to either all nodes validated (PD7, PB8) or to a bounded failure from exhausted refinements (PD6b, PD8, PB3a3, PB3c, PB7b, PB9). These cases partition all terminal states. Hence termination leads to either T or S₅. ∎ A.8.5 Lemma (Invariant Preservation for PDFD) Statement. Across all reachable states of PDFD, the following invariants hold: • Descendant finalization invariant. A node at level i is not considered finally complete unless all nodes in its processed subtree are finalized (guards enforced by PD4a/PD6/PD7). 114 of 186 • Refinement locality. Backtracks always target j = trace_origin(i) with j ≤ i; refinement scope is contiguous and anchored. Proof. • Base Case. The initial state S₀ satisfies both invariants vacuously: no nodes are finalized yet, and no refinement operations have been initiated. Therefore, both the descendant finalization invariant and refinement locality invariant hold trivially. • Inductive Step. Assume both invariants hold in state S. Consider any transition S → S′ according to Table A.8.2. We show that S′ preserves both invariants: o Descendant finalization invariant. Transitions that finalize nodes or advance levels (PD4a, PD6, PD7) are strictly guarded by conditions requiring validated(n) or descendants_validated(n) to be true. These guards explicitly enforce that a node is finalized only when its processed descendants are already finalized. All other transitions either do not affect finalization status or are refinement backtracks that temporarily reset nodes (addressed by refinement locality). o Refinement locality invariant. Backtrack transitions (PD2a, PD3c, PD4b, PD6a) compute the target level j using the trace_origin function, which by definition satisfies j ≤ i. The guard conditions ensure that refinement scope remains contiguous within the range [j, i]. Non-backtrack transitions do not modify refinement relationships. • Conclusion. By induction on the transition sequence, both invariants are preserved across all reachable states. The exhaustive nature of the state transitions in Table A.8.2 guarantees that no invariant-violating state is reachable. ∎ A.8.6 Lemma (Invariant Preservation for PBFD) Statement. Across all reachable states of PBFD: 1. Level-wise ordering. Children/pattern at level i+1 are produced only after Patternᵢ is validated (PB4a). 2. Top-down finalization in completion. PB7/PB8 iterate from level 1 upward without skipping. 3. Refinement locality. Backtracks always target j = trace_origin(i) with j ≤ i; refinement scope is contiguous and anchored (PB3). Proof. • Base Case. The initial state S₀ satisfies all three invariants vacuously: no patterns have been processed, no finalization has begun, and no refinement operations have been initiated. Therefore, all invariants hold trivially in the initial state. • Inductive Step. Assume all three invariants hold in state S. Consider any transition S → S′ according to Table A.8.3. We show that S′ preserves all invariants: o Level-wise Ordering Invariant. The transition PB4a, which advances from Patternᵢ to Patternᵢ₊₁, is strictly guarded by the condition that Patternᵢ is fully validated. This guard ensures that no pattern at level i+1 is produced unless the preceding pattern has been successfully validated. All other transitions either operate within a single level or do not produce new patterns. o Top-down Finalization Invariant. The completion phase transitions (PB7, PB8) progress sequentially through S₄(i) → S₄(i+1), with each step guarded by ∀n ∈ Patternᵢ: processed(n). This ensures that levels are finalized in strict ascending order from 1 to L without skipping. Backtrack transitions from S₄ (PB7a) do not violate this invariant as they temporarily exit completion mode. 115 of 186 o Refinement Locality Invariant. Refinement backtrack transitions (PB3, PB3a2, PB7a) compute the target level j using the trace_origin function, which by definition satisfies j ≤ i. The guard conditions and operational semantics ensure that refinement scope remains contiguous within [j, i]. Nonrefinement transitions do not modify these relationships. • Conclusion. By induction on the transition sequence, all three invariants are preserved across all reachable states. The exhaustive nature of the state transitions in Table A.8.3 guarantees that no invariant-violating state is reachable. ∎ A.8.7 Lemma (Unified Progress) Statement. From any non-terminal state, there exists an enabled transition whose execution causes a strict lexicographic decrease in M. Proof. This is guaranteed by the design of the state machines and measure: By the exhaustive annotation of Tables A.8.2 and A.8.3, for every non-terminal state, at least one transition rule is enabled by its guard condition, and the ΔM for that rule shows a strict lexicographic decrease. This is by construction of the state machines. Lemmas A.8.2 and A.8.3 guarantee that decreases in k₂ and k₁ are well-founded and therefore prevent indefinite stuttering in k₃, k₄. ∎ A.8.8 Theorem (Total Correctness) Statement. PDFD and PBFD always terminate and upon termination satisfy their postconditions: • Terminate in T (all nodes validated) or S₅ (refinement exhausted). • Structural invariants (descendant finalization, refinement locality, level ordering) hold at all reachable states. Proof. Follows directly from Lemmas A.8.2–A.8.7 and the invariant guarantees in A.8.5 and A.8.6: • Termination by Lemma A.8.4. • Partial correctness by Lemmas A.8.5–A.8.6 (invariants). Upon termination in state T, the postcondition ∀n ∈ V, P(n)=2 is met directly by the guard of the terminal rule (PD7/PB8). The structural invariants ensure this final state is internally consistent. • Progress/no stalling by Lemma A.8.7. Therefore both algorithms satisfy total correctness: termination and preservation of required invariants; terminal states meet the declared postconditions. ∎ Corollaries • A.8.2.1 (Boundedness). Total number of refinement attempts ≤ L ⋅ Rₘₐₓ. • A.8.3.1 (Finalization Permanence). Once P(n)=2 outside an active refinement rollback, it remains 2; any temporary reset is only through guarded refinemententry transitions, is bounded by Lemma A.8.2, and is always accompanied by a strict decrease in the k₂ component of the measure M. • A.8.4.1 (Temporal completeness). From start, eventually the run reaches either success T or bounded failure S₅: □(start ⇒ ◊(T ∨ S₅)). A.8.9 Proof Mermaid Code flowchart TD subgraph Foundation [Foundation] A[Tables A.8.1 - A.8.3<br>Definitions & State Rules] 116 of 186 end A --> B[A.8.1<br>Termination Measure M] A --> C[A.8.2<br>Bounded Refinement] A --> D[A.8.3<br>Finalization Invariant] A --> E[A.8.5<br>PDFD Invariants] A --> F[A.8.6<br>PBFD Invariants] C -- proves k₂ property --> G[A.8.4<br>Termination] D -- proves k₁ property --> G C -- provides bound --> H[A.8.7<br>Progress] D -- provides property --> H subgraph Conclusion [Conclusion] I[A.8.8<br>Correctness] end E -- proves --> I F -- proves --> I G -- proves --> I H -- proves --> I A.9 TLE Mermaid Code, Algorithm, and Process Algebra Appendix A.9 provides the formal specification for the Three-Level Encapsulation (TLE) technique, covering its Mermaid diagrams, pseudocode, and CSP model. A.9.1 Structural Workflow Mermaid Code graph TD %% Compact Layout for Single Column subgraph Legend LG1[Level N] LG2[Level N+1] LG3[Level N+2] %% Vertical layout within legend LG1 --- LG2 LG2 --- LG3 end %% Main structure with condensed labels G[Grandparent] --> P1[Parent A] G --> P2[Parent B] G --> P3[Parent C] P1 --> B1[Bitmask A1] P2 --> B2[Bitmask B1] P3 --> B3[Bitmask C1] %% Colors classDef level1 fill:#E1F5FE,stroke:#039BE5 117 of 186 classDef level2 fill:#FFF8E1,stroke:#FBC02D classDef level3 fill:#E8F5E9,stroke:#388E3C class G level1 class P1,P2,P3 level2 class B1,B2,B3 level3 class LG1 level1 class LG2 level2 class LG3 level3 A.9.2 State Machine Mermaid Code stateDiagram-v2 state "S₀: Idle" as S0 state "S₁: Data Loaded" as S1 state "S₂: Hierarchy Resolved" as S2 state "S₃: Children Evaluated" as S3 state "S₄: Children Updated" as S4 state "S₅: Changes Committed" as S5 state "S₆: Workflow Finalized" as S6 [*] --> S0 : TLE1 - System Start S0 --> S1 : TLE2 - initiate_workflow(Grandparent) S0 --> S6 : TLE11 - ¬has_unprocessed_unit() S1 --> S2 : TLE3 - resolve_hierarchy() S2 --> S3 : TLE4 - evaluate_children() S3 --> S4 : TLE5 - update_required ∧ apply_update() S3 --> S5 : TLE6 - ¬update_required S4 --> S5 : TLE7 - persist_changes() S5 --> S0 : TLE8 - has_next_unit() S5 --> S6 : TLE9 - ¬has_next_unit() S6 --> S0 : TLE10 - Workflow Complete A.9.3 Algorithm (Pseudo Code) Algorithm TLE(Pages) Procedure TLE_EventDriven(Units) Input: Units – list of TLE data units (e.g., grandparent entities) to process Output: Tree with bitmask-encoded children selections finalized 1: currentState ← S₀ // TLE1: [*] → S₀. System Start 2: currentUnit ← NULL // TLE process runs continuously, reacting to external events 3: while System_Running do 4: switch currentState 5: case S₀: // Idle (TLE_S0). Awaiting load or finalization signal. 6: // TLE2: load(u) → S₁ | TLE11: no_next_unit(u) → S₆ 7: event ← WaitForEvent({load, no_next_unit}) // Wait for next unit or end-of-batch 8: if event.type == load then 118 of 186 9: currentUnit ← event.Unit // Store the unit parameter (u) 10: currentState ← S₁(currentUnit) 11: else if event.type == no_next_unit then 12: currentUnit ← event.Unit // Unit being finalized (passed from environment) 13: currentState ← S₆(currentUnit) 14: // Note: Unit parameter is always received from the environment here (load/no_next_unit) 15: 16: case S₁(u): // Data Loaded (TLE_S1(u)). Awaiting hierarchy resolution. 17: // TLE3: hierarchy_resolved(u) → S₂ 18: event ← WaitForEvent({hierarchy_resolved}) 19: if event.Unit == u then // Check for unit-specific synchronization 20: resolve_hierarchy() // TLE3 Action (Internal resolution) 21: currentState ← S₂(u) 22: 23: case S₂(u): // Hierarchy Resolved (TLE_S2(u)). Awaiting children evaluation. 24: // TLE4: children_evaluated(u) → S₃ 25: event ← WaitForEvent({children_evaluated}) 26: if event.Unit == u then 27: child_nodes ← evaluate_children() // TLE4 Action: Iterative READ 28: currentState ← S₃(u) 29: 30: case S₃(u): // Children Evaluated (TLE_S3(u)). Conditional path: update or skip. 31: // TLE5: children_updated(u) → S₄ | TLE6: skip_update(u) → S₅ 32: event ← WaitForEvent({children_updated, skip_update}) 33: if event.Unit == u then 34: if event.type == children_updated then // TLE5 (WRITE required) 35: apply_update(child_nodes) // TLE5 Action 36: currentState ← S₄(u) 37: else // event.type == skip_update (TLE6) 38: currentState ← S₅(u) 39: 40: case S₄(u): // Children Updated (TLE_S4(u)). Awaiting changes commit. 41: // TLE7: changes_committed(u) → S₅ 42: event ← WaitForEvent({changes_committed}) 43: if event.Unit == u then 44: persist_changes() // TLE7 Action: COMMIT 45: currentState ← S₅(u) 46: 47: case S₅(u): // Changes Committed (TLE_S5(u)). Signalling readiness or finalization. 48: // TLE8: has_next_unit → S₀ | TLE9: no_next_unit(u) → S₆ 49: // The process emits the readiness/finalization signal and transitions immediately. 50: if HasNextUnitAvailable() then 119 of 186 51: EmitEvent(has_next_unit) // TLE8 Action (Unparameterized signal) 52: currentState ← S₀ // Loop back to S₀ to await new work 53: else 54: EmitEvent(no_next_unit.u) // TLE9 Action (Parameterized signal) 55: currentState ← S₆(u) 56: 57: case S₆(u): // Workflow Finalized (TLE_S6(u)). Final action and system reset. 58: // TLE10: finalize_process(u) → S₀ 59: EmitEvent(finalize_process.u) // TLE10 Action 60: currentState ← S₀ // TLE10: Transition back to S₀ to await new unit 61: 62: end switch 63: end while 64: return End Procedure A.9.4 CSP Implementation and Formal Verification The complete CSPM model (FDR 4.2.7 compatible) implementing all operations from Algorithm A.9.3 and state transitions from Table 48 and Table 49 is available in our supplementary repository. Verification Status: All 49 formal properties were successfully verified, including deadlock freedom, divergence freedom, deterministic behavior, correct sequencing of TLE1–TLE11 transitions, and behavioral conformance to the abstract specification (TLE_Abstract_Process). Unit-specific guarantees such as WaitForEvent(u) synchronization, EmitEvent(u) propagation, and recurrence S₆ → S₀ were validated. Repository Access: GitHub: https://github.com/IBM-Consulting-Formal-Methods/TLE_CSP (commit: 7e5b6c3) The model includes all TLE processes (S0, S1(u), S2(u), S3(u), S4(u), S5(u), S6(u)), event channels, and unit parameterization (u1, u2, u3) as documented in Tables A.9.1 - A.9.2. The repository README provides detailed verification instructions and complete FDR 4.2.7 assertion results. A.9.5 TLE (Three-Level Encapsulation) Technique Tables The TLE technique's formal specification is further detailed through Table A.9.1, which provides a unified set of definitions for both the pseudocode and CSP models. Table A.9.2 then outlines the core CSP process algebra, detailing the state transitions and key events that correspond to the pseudocode. Table A.9.1. TLE Technique - Unified Definitions (Pseudocode + CSP) Pseudocode Term Type Description Pseudocode Lines CSP Mapping Algorithm & States Algorithm TLE(Units) Meta-Process Coordinates the tree-leaf encoding pipeline. Header TLE_Process(start→ TLE_S0) currentState State Variable Tracks the current stage of the TLE process. 1, 4, 10, 13, 21, 28, 36, (Implicit in CSP State Processes TLE_Sₓ(u)) 120 of 186 Pseudocode Term Type Description Pseudocode Lines CSP Mapping 38, 45, 52, 55, 60 S₀ State Idle. Waiting for input. 5, 52, 60 TLE_S0 S₁ State Data Loaded. A TLE unit is loaded. 10, 16 TLE_S1(u) S₂ State Hierarchy Resolved. Parent levels identified. 21, 23 TLE_S2(u) S₃ State Children Evaluated. Child states processed. 28, 30 TLE_S3(u) S₄ State Children Updated. Child states modified. 36, 40 TLE_S4(u) S₅ State Changes Committed. Modifications persisted. 38, 45, 47 TLE_S5(u) S₆ System End State Workflow Finalized. Process complete. 13, 55, 57 TLE_S6(u) Functions & Actions LOAD(Grandparent) Core TLE Op Loads a TLE data unit. 9 load?u:UNIT (Input) resolve_hierarchy() Processing Function Resolves and validates hierarchy. 20 hierarchy_resolved.u (Output) evaluate_children() Processing Function Reads and logically processes children. 27 children_evaluated.u (Output) apply_update(...) Core TLE Op WRITE. Modifies child states. 35 children_updated.u (Output) persist_changes() Core TLE Op COMMIT. Persists changes. 44 changes_committed.u (Output) finalize_process() System Function Completes the TLE algorithm. 59 finalize_process.u (Output) Conditions update_required Condition Trigger for WRITE operation. 34 (Implied by children_updated.u choice in TLE_S3) has_next_unit() Condition / Signal Checks if more units exist. 50 has_next_unit (Output, Valueless) ∃ unprocessed unit... Condition Checks if more units exist. 7 (Implicit in load?u:UNIT choice in TLE_S0) CSP-Specific Events load CSP Input Signals a unit is ready for processing. 7 load?u:UNIT no_next_unit CSP I/O Signals no more units. 7, 11, 48, 54 S0: Input (?u); S5: Output (.u) skip_update CSP Output Signals no update was required, skipping to commit. 32, 37 skip_update.u Table A.9.2. TLE Technique - CSP Process Algebra Core (States + Transitions) CSP Process Key Transitions (TLE Ref.) Pseudocode Lines CSP Events (Simplified) S₀ (TLE_S0) TLE1: Start → S₀ 1 (start→TLE_S0)→TLE_S0 (via TLE_Process) TLE2: load(u) → S₁ 7–10 load?u:UNIT → TLE_S1(u) TLE11: no_next_unit(u) → S₆ 7, 11–13 no_next_unit?u:UNIT → TLE_S6(u) S₁(u) (TLE_S1(u)) TLE3: hierarchy_resolved(u) → S₂ 18–21 hierarchy_resolved.u → TLE_S2(u) 121 of 186 CSP Process Key Transitions (TLE Ref.) Pseudocode Lines CSP Events (Simplified) S₂(u) (TLE_S2(u)) TLE4: children_evaluated(u) → S₃ 25–28 children_evaluated.u → TLE_S3(u) S₃(u) (TLE_S3(u)) TLE5: children_updated(u) → S₄ 32, 34–36 children_updated.u → TLE_S4(u) TLE6: skip_update(u) → S₅ 32, 37–38 skip_update.u → TLE_S5(u) S₄(u) (TLE_S4(u)) TLE7: changes_committed(u) → S₅ 42–45 changes_committed.u → TLE_S5(u) S₅(u) (TLE_S5(u)) TLE8: has_next_unit → S₀ 50–52 has_next_unit → TLE_S0 TLE9: no_next_unit(u) → S₆ 53–55 no_next_unit.u → TLE_S6(u) S₆(u) (TLE_S6(u)) TLE10: finalize_process(u) → S₀ 58–60 finalize_process.u → TLE_S0 Top-Level (TLE_Process) System Start → S₀ 1 start → TLE_S0 A.9.6 Formal Verification Methodology and Scope Verification Framework All analyses were conducted using FDR 4.2.7 with standard behavioral reduction (sbisim, diamond elimination) and breadth-first state exploration. Table A.9.3. Coverage of the 49 Verification Assertions Category Count Coverage Core System Safety 4 Deadlock freedom; behavioral refinement (T, F, FD) State-Level Reliability 38 Two specifications: S₀ (non-param) + S₁–S₆ (3 units each) Liveness Guarantees 2 Divergence checks for TLE_Process and TLE_Abstract_Process Composition & Robustness 5 Concurrency checks (2), hostile-environment checks (2), determinism (1) Total 49 Complete verification of safety, liveness, and concurrency Assertion Breakdown Core System Safety (4): 1. TLE_Process :[deadlock free] 2. TLE_Process [T= TLE_Abstract_Process] 3. TLE_Process [F= TLE_Abstract_Process] 4. TLE_Process [FD= TLE_Abstract_Process] State-Level Reliability (38): • Implementation states: S₀ (1) + S₁–S₆ × (u₁, u₂, u₃) (18) = 19 • Abstract states: Abstract_S₀ (1) + Abstract_S₁–S₆ × (u₁, u₂, u₃) (18) = 19 Liveness Guarantees (2): 1. TLE_Process :[divergence free] 2. TLE_Abstract_Process :[divergence free] Composition & Robustness (5): 1. TLE_TwoUnits :[deadlock free] (parallel composition test) 2. TLE_Abstract_TwoUnits :[deadlock free] (abstract parallel test) 3. TLE_Hostile_System :[deadlock free] (hostile environment robustness) 4. TLE_HostileEnv :[deadlock free] (hostile environment itself) 5. TLE_Process :[deterministic [F]] (internal determinism) Reproducibility All 49 checks can be reproduced by loading the CSP model (tle_model.csp) in FDR 4.2.7 and executing the assertions. The parameterized unit design (u₁, u₂, u₃) enables tractable exploration of both sequential and concurrent scenarios, with all assertions passing consistently. A.10 Proofs of TLE Theorems 128 of 186 Table A.11.1. PDFD MVP application state descriptions and their mappings to generic PDFD state categories and parameter configurations State ID Phase Description Generic Mapping (State + Parameters) S1 Process & Validate Level 1 Root node (Node 1) S₁(1) → S₂(1) S2 Process & Validate Level 2 Nodes 2.1 and 2.2 S₁(2) → S₂(2) S3 Process & Validate Level 3 Nodes 3.1 and 3.2 S₁(3) → S₂(3) S4 Process & Validate Level 4 Nodes 4.1 and 4.2 S₁(4) → S₂(4) S5 Process & Validate Level 5 Nodes 5.1 and 5.2 S₁(5) → S₂(5) S6 Process & Validate Level 6 Nodes 6.1 and 6.2 S₁(6) → S₂(6) S2_R1 Refine Levels 2-3 Reprocess Levels 2-3 due to failure at Level 3 S₁(j=2) → S₂(j=2) S2_R2 Refine Levels 2-4 Reprocess Levels 2-4 due to failure at Level 4 S₁(j=2) → S₂(j=2) S2_R3 Refine Levels 2-5 Reprocess Levels 2-5 due to failure at Level 5 S₁(j=2) → S₂(j=2) S7 Finalize Level 5 Subtree Finalize subtree under 5.1 and 5.2 S₃(5) S8 Finalize Level 4 Subtree Finalize subtree under 4.1 and 4.2 S₃(4) S9 Finalize Level 3 Subtree Finalize subtree under 3.1 and 3.2 S₃(3) S10 Finalize Level 2 Subtree Finalize subtree under 2.1 and 2.2 S₃(2) S11 Finalize Root Subtree Finalize root node and ensure completeness S₄(1) S_ERROR Terminate on Failure Refinement limit exceeded or validation failed S₅ Table A.11.2. PDFD MVP state transition rules, triggers, and their corresponding formal definitions in the generic PDFD model Rule ID From State -> To State Formal Condition / Trigger Workflow Step Generic Rule (PD# + Parameters ) PDFD1 [*] → S1 System initialized Begin root-level processing PD1 PDFD2 S1 → S2 Root validated Advance to Level 2 PD2b (i=1) PDFD3 S2 → S3 Level 2 validated Advance to Level 3 PD2b (i=2) PDFD4 S3 → S2_R1 Level 3 validation failed Backtrack to refine Levels 2-3 PD2a (i=3, j=2) PDFD5 S2_R1 → S3 Levels 2-3 refinement validated Revalidate Level 3 PD3b (j=2→i=3) PDFD6 S3 → S4 Level 3 validated Advance to Level 4 PD2b (i=3) PDFD7 S4 → S2_R2 Level 4 validation failed Backtrack to refine Levels 2-4 PD2a (i=4, j=2) PDFD8 S2_R2 → S4 Levels 2-4 refinement validated Revalidate Level 4 PD3b (j=2→i=4) PDFD9 S4 → S5 Level 4 validated Advance to Level 5 PD2b (i=4) PDFD10 S5 → S2_R3 Level 5 validation failed Backtrack to refine Levels 2-5 PD2a (i=5, j=2) PDFD11 S2_R3 → S5 Levels 2-5 refinement validated Revalidate Level 5 PD3b (j=2→i=5) PDFD12 S5 → S6 Level 5 validated Advance to Level 6 PD2b (i=5) PDFD13 S6 → S7 Level 6 validated Finalize Level 5 subtrees PD4 (i=6) PDFD14 S7 → S8 Subtree at Level 5 validated Finalize Level 4 subtrees PD4a PDFD15 S8 → S9 Subtree at Level 4 validated Finalize Level 3 subtrees PD4a PDFD16 S9 → S10 Subtree at Level 3 validated Finalize Level 2 subtrees PD4a PDFD17 S10 → S11 Subtree at Level 2 validated Finalize root node PD5 PDFD18 S11 → [*] Root finalized Terminate PD6 → PD7 129 of 186 Rule ID From State -> To State Formal Condition / Trigger Workflow Step Generic Rule (PD# + Parameters ) PDFD19 S2_R1/S2_R2/S2_R3 → S_ERROR Refinement validation failed AND refinement_attempts[2] ≥ 60 Terminate PD3c → PD8 PDFD20 S3/S4/S5 → S_ERROR refinement_attempts[2] ≥ 60 Terminate PD8 For simplicity, the level-by-level top-down process in the generic model is compacted and replaced by S11’s subtree top-down state, governed by the PDFD18 rules. While the formal state categories (S₁, S₂, S₃, S₄, and S₅) follow the definitions in Section 3.4.1, this particular state machine reflects the actual control flow of the MVP implementation and does not enumerate all possible scenarios defined by the generic PDFD methodology. The table captures the practical subset of transitions that occurred during execution and validation of the MVP system. In this MVP, bottom-up subtree finalization (S₃(i)) culminates in a top-down global finalization pass (S₄(1)), recognizing the root-driven pass as a streamlined final step. The state machine diagram (see Figures A.11.3) visually depicts the flow, with transitions corresponding to the rules in Table A.11.2. Please refer to Appendix A.12 for the State Machine Mermaid code. A.11.6. Development Process For detailed step-by-step implementation traces of the MVP, including screenshots, transaction sequences, and database evolution, refer to Appendix A.13. A.11.7. Key Technical Highlights This MVP implementation illustrates the practical strengths of the Primary DepthFirst Development (PDFD) methodology through several key technical highlights: • Controlled Depth Parallelism (BF-by-Two Adaptation): o Benefit: By processing two sibling nodes in parallel at each hierarchical level during the depth-first traversal, the system can expose cross-branch inconsistencies and UI state conflicts early in development, rather than deferring them to integration. o Contrast: A pure DFD approach may postpone the detection of lateral interactions until deeper refinement phases, whereas a pure BFD approach—by prioritizing horizontal breadth—may introduce significant coordination overhead and delay cross-level dependency validation. o Example: Simultaneously testing the nodes “Asia” and “North America” at the continent level revealed UI inconsistencies in regional naming conventions (e.g., “state” in the US vs. “province” in China). Early resolution of these discrepancies prevented cascading structural conflicts at deeper country-specific levels of the hierarchy. • Iterative Schema Refinement o Benefit: The integration of CDD allows for flexible schema evolution during the development process, accommodating necessary mid-development changes such as the introduction of surrogate keys. o Contrast: Traditional, more rigid development methodologies like Waterfall, with their upfront and inflexible schema design, often hinder the incorporation of necessary updates identified later in the cycle. o Example: Initially, composite keys (e.g., combining PersonId and ContinentId) were used. However, during backtracking at the continent level, these were refactored to simpler surrogate keys (e.g., SelectedContinentId), significantly simplifying downstream data relationships and query logic. 130 of 186 Figure A.11.3. State machine diagram for the PDFD MVP showing progression, refinement, and termination paths mapped to formal rule identifiers • Hierarchical Backtracking o Benefit: Backtracking to previously validated hierarchical levels to incorporate new branches enhances the stability and reusability of the developed components by ensuring core paths are solid before extensive horizontal expansion. o Contrast: Monolithic development methods often require significant rework or even rollback when errors are discovered late in the process, especially after substantial horizontal expansion. o Example: After thoroughly validating the path USA → Maryland → Howard, PDFD facilitated backtracking to the state level to add branches for Virginia. This allowed for the reuse of existing controllers and views, minimizing redundant development effort. 131 of 186 • Methodological Cohesion o The PDFD methodology effectively integrates DFD, BFD through the BFby-Two strategy, and CDD. o This MVP serves as a practical instantiation of the hybrid approach, demonstrating its ability to maintain the formal properties of the underlying methodologies (as discussed in Section 3.4.1) while offering a pragmatic and adaptable development process for hierarchical systems. A.12 PDFD MVP State Machine Workflow Mermaid Code A.12.1 Mermaid Code for Figure A.11.3 stateDiagram-v2 direction TB [*] --> S1 state S1: Process & Validate Level 1 S1 --> S2: PDFD2 - Root Validated state S2: Process & Validate Level 2 S2 --> S3: PDFD3 - Level 2 Validated state S3: Process & Validate Level 3 S3 --> S4: PDFD6 - Level 3 Validated S3 --> S2_R1: PDFD4 - Validation Failed S3 --> S_ERROR: PDFD20 - attempts≥60 state S2_R1: Refine Levels 2-3 S2_R1 --> S3: PDFD5 - Refinement Validated S2_R1 --> S_ERROR: PDFD19 - Failed & attempts≥60 state S4: Process & Validate Level 4 S4 --> S5: PDFD9 - Level 4 Validated S4 --> S2_R2: PDFD7 - Validation Failed S4 --> S_ERROR: PDFD20 - attempts≥60 state S2_R2: Refine Levels 2-4 S2_R2 --> S4: PDFD8 - Refinement Validated S2_R2 --> S_ERROR: PDFD19 - Failed & attempts≥60 state S5: Process & Validate Level 5 S5 --> S6: PDFD12 - Level 5 Validated S5 --> S2_R3: PDFD10 - Validation Failed S5 --> S_ERROR: PDFD20 - attempts≥60 state S2_R3: Refine Levels 2-5 S2_R3 --> S5: PDFD11 - Refinement Validated S2_R3 --> S_ERROR: PDFD19 - Failed & attempts≥60 state S6: Process & Validate Level 6 S6 --> S7: PDFD13 - Level 6 Validated state S7: Finalize Level 5 S7 --> S8: PDFD14 - Subtree Validated 132 of 186 state S8: Finalize Level 4 S8 --> S9: PDFD15 - Subtree Validated state S9: Finalize Level 3 S9 --> S10: PDFD16 - Subtree Validated state S10: Finalize Level 2 S10 --> S11: PDFD17 - Subtree Validated state S11: Finalize Root S11 --> [*]: PDFD18 - Root Finalized state S_ERROR: Terminate on Failure S_ERROR --> [*] A.13 PDFD MVP Development Process This section details the step-by-step progression of the PDFD MVP’s development process; the corresponding source code is provided in [28]. A.13.1 Root Node Level – Visitor The root node (Node 1 in Figure A.13.1) represents visitor information, serving as the entry point for the application’s hierarchical workflow. Figure A.13.1. PDFD MVP Root Node (Visitor Entry) User Interface Implementation Details • Model: The Person class maps to the Persons database table (Table A.13.1), with PersonId as the primary key. • Controller: The PersonsController processes HTTP requests, binds the Person model to the view, and handles form submissions. • View: ASP.NET Razor syntax is used to render the visitor entry interface (Figure A.13.1). • Workflow: Users input visitor details, which are persisted in SQL Server (Table A.13.1) upon submission. This process, representing Level 1 (S1 in Figure A.11.3), then redirects users to the Continent Level (Level 2) via PDFD2 (Table A.11.2). Table A.13.1. Sample Data for Person (Root Level) in PDFD MVP Hierarchy PersonId First Name Middle Name Last Name Email 1 Test T Tester [email protected]m A.13.2 Continent Level – Asia and North America This level handles continent selection and integrates with downstream geographical hierarchies. 1. Implementation Overview 133 of 186 Table A.13.2 outlines the key components, including models, database tables, and core data fields. Table A.13.2. Model, Database Table, and Data Field Summary for PDFD MVP Continent Level Model SQL Table Function Key Data Fields Continent Continents Reference Data ContinentId, Name, NameTypeId SelectedContinent SelectedContinents Selection Tracking SelectedContinentId, PersonId, ContinentId, IsDeleted ContinentViewModel N/A View Model ContinentId, ContinentName, PersonId, IsSelected 2. Source Tables The PDFD MVP uses the following tables as source data, with some shared across all hierarchy levels: • Persons (Table A.13.1) – Shared across all levels • Continents (Table A.13.3) • NameTypes (Table A.13.4) – Shared across all levels • SelectedContinents (Table A.13.5) Table A.13.3. Reference Data for Continents in PDFD MVP ContinentId Name NameTypeId 1 Asia 1 2 North America 1 Table A.13.4. Reference Data for NameTypes (Hierarchy Levels) in PDFD MVP NameTypeId Name 1 Continent 2 Country 3 State 4 County 5 City 6 District 7 Province 11 Region Table A.13.5. Sample Transaction Data for SelectedContinents in PDFD MVP SelectedContinentId PersonId ContinentId IsDeleted 1 1 1 1 2 1 2 0 3. Workflow Logic User Interaction • Users interact with the continent selection interface (Figure A.13.2), which triggers updates to the SelectedContinents table (Table A.13.5). Upon submission, the system updates Table A.13.5 according to the following rules—also applicable at subsequent hierarchy levels: o New selections are added with IsDeleted = 0. o Deselections are marked with IsDeleted = 1 (soft delete). o Restored selections have IsDeleted reset to 0. • User selections at the continent level trigger cascaded updates to downstream levels (e.g., countries). 134 of 186 Figure A.13.2. PDFD MVP Continent Selection User Interface State Machine (Figure A.11.3) • Level 2 (S2) processed. • Transitions to Level 3 (S3) follow PDFD3 (∑P(n) ≥ K₂). Structural Workflow (Figure A.11.1) • Level 2 with K₂ = 2: o Node 2.1: North America (ContinentId = 2) o Node 2.2: Asia (ContinentId = 1) 4. Hierarchical Context Refinement Logic (Figure A.11.3) • Errors detected at Level 3 (S3) trigger refinement starting at Jᵢ=2 (PDFD4). A.13.3 Country Level – United States and Canada This level manages country selection within the continent hierarchy. 1. Implementation Overview CDD Intervention (Figure A.11.3) • Missing IsSelected field triggered refinement (PDFD4) for Levels 2–3. • Post-refinement, processing resumed at Level 3 (PDFD5). Models • Country, SelectedCountry, CountryViewModel (see Table A.13.6) Tables • Countries Lookup (Table A.13.7), SelectedCountries Transaction Data (Table A.13.8) Table A.13.6 summarizes the models, corresponding tables, functions, and their roles at the country level. Table A.13.6 Model, Database Table, and Data Field Summary for PDFD MVP Country Level Model SQL Table Function Key Data Fields Country Countries Reference Data CountryId, Name, ContinentId, NameTypeId SelectedCountry SelectedCountries Selection Tracking SelectedCountryId, SelectedContinentId, CountryId, IsDeleted CountryViewModel N/A View Model CountryId, CountryName, SelectedContinentId, IsSelected Table A.13.7 Reference Data for Countries in PDFD MVP CountryId Name ContinentId NameTypeId 1 USA 2 2 2 Canada 2 2 Table A.13.8 Sample Transaction Data for SelectedCountries in PDFD MVP SelectedCountryId SelectedContinentId CountryId IsDeleted 1 2 1 0 135 of 186 SelectedCountryId SelectedContinentId CountryId IsDeleted 2 2 2 1 2. Workflow Logic User Interaction The CountryController uses the CountryViewModel to populate the interface (Figure A.13.3), where users toggle country selections (e.g., USA, Canada). Changes are persisted to the SelectedCountries table (Table A.13.8) using soft deletion (IsDeleted flag). Figure A.13.3. PDFD MVP Country Selection User Interface Pre-Checked Entries Previously selected countries (e.g., USA in Table A.13.8) are pre-checked in the interface, reflecting historical data stored in SelectedCountries. • State Machine (Figure A.11.3) o S3 processing step failed o Transitions to S2_R1 • Structural Workflow (Figure A.11.1) Level 3 with 𝐾3 = 2 (indicating two nodes processed at this level): o Node 3.1: USA (CountryId = 1) o Node 3.2: Canada (CountryId = 2) A.13.4 State Level – Maryland and Virginia This level handles state/province selection within countries, adhering to the hierarchical structure defined in PDFD. It is state S4 in Figure A.11.3. Here, a surrogate key was found to be a better choice for database design, prompting the use of the CDD strategy to refine levels 2-4. Refer to 'Transition from Composite to Surrogate Keys' in item 1 of section A.13.7, curve b in Figure A.11.1, and state S2_R2 in Figure A.11.3 for more details. 1. Implementation Overview CDD Intervention (Figure A.11.3) • Surrogate key introduction triggered refinement (PDFD7) for Levels 2–4. • Processing resumed at Level 4 (PDFD8). Models • State, SelectedState, StateViewModel. (Table A.13.9) Tables • States Lookup (Table A.13.10), SelectedStates (Table A.13.11) Table A.13.9 summarizes the models, corresponding tables, functions, and their roles at the state level. Table A.13.9. Model, Database Table, and Data Field Summary for PDFD MVP State Level Model SQL Table Functions Key Data Fields State States Reference Data StateId, Name, CountryId, NameTypeId 136 of 186 Model SQL Table Functions Key Data Fields SelectedState SelectedStates Selection Tracking SelectedStateId, SelectedCountryId, StateId, IsDeleted StateViewModel N/A View Model StateId, StateName, SelectedCountryId, IsSelected Table A.13.10. Reference Data for States in PDFD MVP StateId Name CountryId NameTypeId 1 Maryland 1 3 2 Virginia 1 3 Table A.13.11. Sample Transaction Data for SelectedStates in PDFD MVP SelectedStateId SelectedCountryId StateId IsDeleted 1 1 1 0 2 1 2 1 2. Workflow Logic User Interaction • The StateController uses the StateViewModel to populate the interface (Figure A.13.4), where users toggle state selections (e.g., Maryland, Virginia). Changes are saved to the SelectedStates table (Table A.13.11) using soft deletion (IsDeleted flag). Figure A.13.4. PDFD MVP State Selection User Interface • Users modify state selections, with pre-checked entries reflecting prior choices stored in SelectedStates. State Machine (Figure A.11.3) • Level 4 processing • Transitions to S2_R2 (PDFD7) Structural Workflow (Figure A.11.1) Level 4 with 𝐾4 = 2 (indicating two nodes processed at this level): • Node 4.1: Maryland (StateId = 1) • Node 4.2: Virginia (StateId = 2) A.13.5 County Level – Howard and Baltimore This level manages county/district selection within states, corresponding to S5 in Figure A.11.3's 'Processing & Refinement' state. A missing IsDeleted field at this stage triggered the CDD methodology to refine levels 2-5. For details, refer to 'Introduction of the IsDeleted Flag' in A.11.7.1, curve c in Figure A.11.1, and S2_R3 in Figure A.11.3. 1. Implementation Overview CDD Intervention (Figure A.11.3) • Missing IsDeleted flag triggered refinement (PDFD10) for Levels 2–5. • Processing resumed at Level 5 (PDFD11). Models • County, SelectedCounty, CountyViewModel (Table A.13.12) 137 of 186 Tables • Counties Lookup (Table A.13.13), SelectedCounties Transaction Data (Table A.13.14) Table A.13.12. Model, Database Table, and Data Field Summary for PDFD MVP County Level Model SQL Table Function Key Data Fields County Counties Reference Data CountyId, Name, StateId, NameTypeId SelectedCounty SelectedCounties Selection Tracking SelectedCountyId, SelectedStateId, CountyId, IsDeleted CountyViewModel N/A View Model CountyId, CountyName, SelectedStateId, IsSelected Table A.13.13. Reference Data for Counties in PDFD MVP CountyId Name StateId NameTypeId 1 Howard 1 4 2 Boltimore 1 4 Table A.13.14. Sample Transaction Data for SelectedCounties in PDFD MVP SelectedCountyId SelectedStateId CountyId IsDeleted 1 1 1 0 2. Workflow Logic User Interaction • Users toggle county selections (e.g., Howard, Baltimore) within Maryland via the interface (Figure A.13.5), with updates persisted to SelectedCounties (Table A.13.14). Figure A.13.5. PDFD MVP County Selection User Interface State Machine (Figure A.11.3) • Level 5 processing • Transitions to S2_R3 (PDFD10) Structural Workflow (Figure A.11.1) Level 5 with 𝐾5 = 2 (indicating two nodes processed at this level): • Node 5.1: Howard County (CountyId = 1) • Node 5.2: Baltimore County (CountyId = 2) A.13.6 City Level – Ellicott City and Columbia This level handles city selection within counties. 1. Implementation Overview Models • City, SelectedCity, CityViewModel (Table A.13.15) Tables • Cities Lookup (Table A.13.16), SelectedCities Transaction Data (Table A.13.17) 144 of 186 The visual conventions used in Figure A.14.1 are defined as follows: Node Conventions • Root Node: Level 1 (ContinentGrandparent) • Numbering: First digit = level, second digit = position (e.g., Node 3.1 = North America) Annotations • Arrows: Progression through hierarchical levels • Dotted Lines: Unselected nodes • Curve a: CDD-driven refinements (Levels 1–3) triggered by Level 3 failures A.14.5 State Machine Representation The PBFD MVP is captured by a specialized state machine (see Tables A.14.1 & A.14.2). Several PBFD states integrate level processing plus TLE-based resolution for subsequent levels (e.g., Level_3_Processing_Validating_Resolving handles levels 3–5 as a single TLE scope). This coalescing reduces protocol overhead and mirrors the encapsulated access patterns characteristic of columnar and encoded storage architectures [53,55]. Key note: While the MVP’s state transitions preserve the generic PBFD semantics— progression, refinement, and finalization—they are implemented in a simplified and consolidated form. The MVP employs coarser TLE-scoped states to optimize data transfer volume and improve query efficiency. Generic mapping and rules in Tables A.14.1 - A.14.2 are defined in Tables 39 and 40. Table A.14.1. PBFD MVP-specific state definitions with corresponding TLE scopes (functioning as dynamic traversal windows) and generic rule mappings State Id Label Phase Generic Mapping TLE Scope S0 Level_1_Processing_Validating_Resolving Process & Validate Level 1 & resolve Level 2 (TLE Root: ContinentGrandparent) S₁(1) → S₂(1) → S₃(1) Levels 1–3 S1 Level_2_Processing_Validating_Resolving Process & Validate Level 2 & resolve Level 3 (TLE Root: ContinentParent) S₁(2) → S₂(2) → S₃(2) Levels 2–4 S2 Level_3_Processing_Validating_Resolving Process & Validate Level 3 & resolve Level 4 (TLE Root: a continent) S₁(3) → S₂(3) → S₃(3) Levels 3–5 S3 Level_4_Processing_Validating_Resolving Process & Validate Level 4 & resolve Level 5 (TLE Root: a country) S₁(4) → S₂(4) → S₃(4) Levels 4–6 S4 Level_5_Processing_Validating Process & Validate Level 5 (TLE Root: a state) S₁(5) → S₂(5) Levels 5–7 S5 Refine_Level1-3 Refine Levels 1–3 (Level 3 failure) S₁(j) → S₂(j) → S₃(j) (j=1) Levels 1–3 S6 Finalize_All Finalize all nodes top-down S₄(1) → ... → S₄(7) Levels 1–7 S7 Complete Termination state T – S8 Validation_Failure Terminate due to Rₘₐₓ = 50 exhaustion S₅ – Table A.14.2. Unified state transitions for PBFD MVP, integrating generic rule references and workflow logic Rule ID From State To State Condition Generic Rule Workflow Step PBFD1 [*] S0 Start PB1 Initialize Level 1 (TLE 1–3) PBFD2 S0 S1 Level 1 validated & resolved PB4a Proceed to Level 2 (TLE 2–4) PBFD3 S1 S2 Level 2 validated & resolved PB4a Proceed to Level 3 (TLE 3–5) PBFD4 S2 S3 Level 3 validated & resolved PB4a Proceed to Level 4 (TLE 4–6) 145 of 186 Rule ID From State To State Condition Generic Rule Workflow Step PBFD5 S3 S4 Level 4 validated & resolved PB4a Proceed to Level 5 (TLE 5–7) PBFD6 S2 S5 Level 3 validation failed PB3 Refine Levels 1-3 PBFD7 S5 S0 Levels 1-3 reprocessed PB3a Resume Level 1 (TLE 1–3) PBFD8 S5 S8 refinement_attempts ≥ Rₘₐₓ PB9 Terminate with error PBFD9 S4 S6 Level 5 validated PB4b Finalize all levels PBFD10 S6 S7 All nodes finalized. Finalization (S6) combines PB7 and PB8, resolving all levels top-down in a single step for efficiency. PB8 Complete The state machine representation visually depicts the flow of the PBFD application, as shown in Figure A.14.2. The transitions between states correspond to the progression and refinement steps of the methodology, with each transition labeled according to the rules defined in Table A.14.2. State S5 (Refine_Level1-3, PBFD6) reprocesses Levels 1–3 to resolve inconsistencies before resuming at Level 1. Mermaid code for Figure A.14.2 is provided in Appendix A.15. Figure A.14.2. State machine diagram for PBFD MVP, showing pattern transitions and completion rules across hierarchical levels 146 of 186 A.14.6 Data Structure and Relationships The PBFD MVP relies on a hierarchical, pattern-driven relational schema to represent and traverse location-based data. This structure underpins both the backend logic and the dynamic frontend traversal behavior governed by the TLE Rule (see Section 4.2). 1. Sample Locations Dataset At the heart of the PBFD MVP system lies the Locations table (Table A.14.3) — a static reference structure containing all nodes and their hierarchical relationships. This metadata table serves as the input for dynamically generating the grandparent-level tables that form the three-level traversal model. Table A.14.3. Static Locations dataset schema supporting PBFD pattern traversal and bitmask encoding Id Name Name Type Id Type Parent Id Child Id Level 0 ContinentGrandparent null INT null 0 1 1 ContinentParent null INT 0 0 2 2 North America 1 INT 1 0 3 3 South America 1 INT 1 1 3 9 United States 2 BIGINT 2 0 4 10 Canada 2 INT 2 1 4 14 Brazil 2 INT 3 0 4 38 Virginia 3 VARCHAR(120) 9 11 5 45 Maryland 3 INT 9 18 5 102 Howard County 4 INT 45 12 6 148 Ellicott City 5 INT 102 1 7 Explanation of Key Fields • Id: Unique identifier for the node • Name: Entity name (e.g., "North America", "Maryland") • Name Type Id: Categorize the entity type (e.g., continent = 1, country = 2). ContinentGrandparent and ContinentParent are structural placeholders for TLE • Type: The SQL data type for the node's bitmask, determined by the maximum number of children: o INT: Supports up to 32 child selections o BIGINT: Supports up to 64 child selections o VARCHAR(X): For >64 children, storing a character-based bitmask representation • Parent Id: References the parent node's Id • Child Id: The node's zero-based position within its parent's bitmask encoding • Level: The node's depth in the hierarchy The ChildId enables constant-time bitwise operations for setting, clearing, and testing selection flags, minimizing computational overhead once the target row is accessed [53,55]. 2. Design Rationale This static table design supports: • Hierarchical Querying: ParentId define the tree structure. • Pattern Encoding: ChildId enables bitmask-based grouping within TLE tables. • Dynamic Generation: Serves as input to recursively generate TLE tables at runtime, adapting bitmask data types as needed for flexibility. 147 of 186 • Consistency: Levels 1–5 follow a consistent schema; Levels 6–7 are embedded as bitmasks within parent levels. 3. Integration with TLE Every TLE-compliant grandparent table derives its structure from the Locations table: • ParentId defines column-to-row relationships. • ChildId defines the bit position in the bitmask. Example: • "United States" (ChildId = 0) → 0b0001 = bitmask 1 • "Canada" (ChildId = 1) → 0b0010 = bitmask 2 This approach of replacing deep recursive joins with precomputed, encoded tables reduces I/O and aligns with design rationales in columnar storage systems [53,55], though it introduces the operational complexity of dynamic schema generation— a trade-off that aligns with foundational database architecture principles, where encoded storage and performance optimizations often necessitate increased system complexity [134]. A.14.7 Three-Level Encapsulation (TLE) Rule PBFD applies the TLE (Three-Level Encapsulation) rule to model each three-level span in the hierarchy using a single table. This design maps a contiguous span (grandparent→parent columns→child bitmask) into one table, enabling one-hop reads from a root record to its grandchild selections and avoiding multi-join traversal for pattern queries. This approach is analogous to materialized or denormalized encodings used in high-performance DBMS designs (columnar and encoded stores) [53,55,118]. For optimization purposes, the handling of the final three-level span, encompassing the lowest two hierarchical levels, deviates from the standard dynamic table generation. Example of a TLE Unit In a regional structure (see Figure A.14.3): Figure A.14.3 Example of a Three-Level Encapsulation (TLE) unit mapping levels 2–4 in the PBFD hierarchy • Grandparent (Level 2): ContinentParent (Grandparent, Node 2) • Parent (Level 3): [North America], [South America], etc. (Parent columns, Nodes 3.1 – 3.7) • Child (Level 4): Bitmask for selected countries within each continent (Child state, Nodes 4.1 – 4.6) Grandparent Table Hierarchy The hierarchy begins at the conceptual ContinentGrandparent (Level 1) and extends downward. The fictitious top-level nodes (ContinentGrandparent, ContinentParent) act as structural sentinels [135]—providing a stable anchor for the TLE encapsulation boundaries. They prevent root-level special cases and allow the TLE pattern to be applied uniformly across all hierarchical segments. Table A.14.4 summarizes the TLE scope for the three-level segments. 148 of 186 Table A.14.4. Mapping of hierarchical levels to TLE units in PBFD MVP, including node roles and bitmasks Level Grandparent Node (Table) Parent Nodes (Columns) Child Nodes (Bitmask) Three-Level Scope 1 ContinentGrandparent Continentparent Continent selections (e.g. North America (1)) Levels 1–3 2 Continentparent e.g. Asia, North America Country selections (e.g. United States (1)) Levels 2–4 3 Continent e.g. United States, Canada State selections (e.g., Maryland (262,144)) Levels 3–5 4 Country e.g. Virginia, Maryland County selections (e.g., Howard County (4096)) Levels 4–6 5 State e.g. Howard County, Baltimore County City selections (e.g., (Columbia MD + Ellicott City) (3)) Levels 5–7 Note: Parenthesized values represent decimal bitmasks. Handling the Lowest Two Hierarchical Levels As the asymptotic analysis in Appendix A.16 demonstrates, the lowest hierarchical levels in a perfect ternary tree contain approximately 89% of all nodes. To mitigate the potential explosion of dynamic tables, the PBFD methodology leverages TLE’s hierarchical encapsulation by embedding Levels 6 (County) and 7 (City) into their grandparent table (State, Level 5): • County Level (Level 6): Represented as dedicated columns within the State table (Level 5) • City Level (Level 7): Stored as bitmasks within the corresponding County columns This embedding minimizes the number of dynamic tables and preserves compact storage. Table A.14.5 (Dynamic Table Maryland (Level 5)) illustrates this structure, where counties are represented as columns, and city selections are stored as bitmasks within those columns for a specific state. Table A.14.5. Bitmask-encoded dynamic table for Maryland (Level 5), illustrating embedded county/city selections PersonId Howard County (bitmask) …… 1 3 …… Justification This TLE-based relational design provides several key benefits: • It encapsulates the grandparent-parent-child hierarchy within a single unit, using bitmasks for O(1) updates and enabling parallel resolution of nodes within a pattern. • Leveraging the analytical findings from Appendix A.16, it avoids creating hundreds of tables for leaf-level data by embedding their states, thus maintaining modularity and performance despite the exponential node growth in deeper levels. • Scalability Alignment: By minimizing dynamic table proliferation and maintaining compact storage, this approach supports the horizontal scaling and operational efficiency required in cloud-native environments. A.14.8 Database Implementation (SQL Server) The PBFD MVP backend uses SQL Server and combines static tables with dynamically generated Three-Level Encapsulation (TLE) tables. This design replaces deep 149 of 186 recursive joins with compact, schema-on-demand structures optimized via bitmask encoding [90]. Dynamic TLE Table Generation Dynamic tables are derived from the static Locations lookup table through an automated transformation pipeline. Rather than storing each hierarchical level in a fully normalized chain of joins, PBFD generates three-level encapsulated tables that encode grandparent–parent–child relationships. Bitmask columns encode child selections as binary flags, enabling constant-time set, clear, and test operations within SQL Server. Algorithm: Dynamic TLE Table Generator Let • N denote the current hierarchical level • L denote the maximum depth of the hierarchy (in PBFD MVP, L=7) • The algorithm iterates from level 1 to L - 2, generating one dynamic table per grandparent node Input: • Locations metadata (table or JSON) • Maximum dynamic depth = 5 (up to the State level) Output: • SQL table per grandparent that follows the TLE rule (level N) • One column per parent (level N+1) • One bitmask field encoding child selections (level N+2) Steps: 1. Load the Locations data 2. Group nodes by hierarchical level 3. For each level N from 1 to L-2: For each node at level N, generate a dynamic table corresponding to that grandparent node, with: o One column for each parent node at level N+1 o One bitmask field encoding child selections at level N+2 4. Skip dynamic table creation for the lowest two levels (L−1 and L): o These levels are embedded into their grandparent’s table as described in Appendix A.14.7, using dedicated columns and bitmask fields This approach scales to arbitrary depth while maintaining constant-time lookup and update via bitwise operations. It reflects principles seen in schema-on-read and evolutionoriented persistence models [90]. Example root-level table: • ContinentGrandparent (Level 1, Id = 0) • Serves as the hierarchical entry point and contains bitmask columns for descendant states or subregions Operational Safeguards and Deployment To prevent schema drift or runtime faults: • Deterministic CREATE TABLE generation occurs as part of controlled deployment scripts. • All DDL changes are executed inside transactions to ensure rollback safety. • Preflight checks validate bitmask width, column compatibility, and backward consistency before applying any schema upgrades. • Type escalation (e.g., INT → BIGINT → VARCHAR) is handled automatically when child-node cardinality outgrows the existing bitmask type. These safeguards align with established practices in schema evolution and controlled denormalization within polyglot persistence systems [90]. Integrated Schema Structure 150 of 186 The resulting database consists of: Static Tables: • Persons (core entity table) • Locations (full hierarchy metadata) • NameTypes (categorization of nodes: continent, country, etc.) Dynamic TLE Tables (auto-generated): • Level 1: ContinentGrandparent • Level 2: ContinentParent • Level 3: one table per continent (e.g., NorthAmerica, Asia, etc.) • Level 4: one table per country (e.g., [United State], Canada, etc.) • Level 5: one table per state (e.g., Alabama, California, etc.) • Lower levels embedded via bitmask columns rather than additional tables Figure A.14.4 illustrates: • The Persons table as the static entry point • Dynamically generated TLE structures for the first three hierarchical levels • One-hop access paths from Persons • Clear delineation of bitmask fields and level boundaries within each dynamic table Clear delineation of hierarchical roles—table name as grandparent, columns as parents, and bitmask fields as children—within each dynamic TLE table. Figure A.14.4. PBFD MVP database schema integrating static and dynamic TLE-compliant tables with bitmask encoding A.14.9 PBFD Loosely Coupled Table Design Benefits PBFD's dynamic Three-Level Encapsulation (TLE) design replaces rigid, deeply joined schemas with a scalable, loosely coupled architecture. This approach preserves the core advantages of relational databases while systematically addressing common performance and operational bottlenecks. The benefits are summarized in the tables below. 151 of 186 Table A.14.6. Key relational database benefits preserved in PBFD MVP’s TLE-based design Feature Benefit Normalization [136] Static tables are highly normalized. Security [137] Table-level permissions enforce granular access control (e.g., permitting team-specific access to regional data), a foundational relational security model. Optimization [55,138] Each grandparent table can utilize separate indexes and be independently partitioned or sharded, allowing for targeted performance tuning. Table A.14.7. Relational challenges and PBFD MVP’s architectural solutions Challenge PBFD Solution Multi-Table Joins [139] Replaces 4–5 join traversals with direct, one-hop access to precomputed grandparent tables, dramatically reducing query complexity. ORM/Workflow Complexity [140] Employs a single controller and view model across all hierarchical levels, simplifying the application layer and minimizing code duplication. Backup/Restore Bottlenecks [141] Enables modular, table-level operations (e.g., backing up only the "Europe" dataset), which aligns with modern, cloud-native operational practices [90]. The empirical benefits observed in the MVP stem from three key design outcomes: (a) a significant reduction in joins per pattern query, (b) a compact bitmask representation that lowers I/O for read-heavy paths, and (c) a table-level granularity that facilitates independent management. This architectural strategy embodies a practical form of denormalization, trading initial schema complexity for sustained query and operational efficiency, a trade-off well-documented in literature on schema evolution and polyglot persistence. A.14.10 Development Process The PBFD MVP follows a top-down hierarchical construction guided by the central Locations metadata table and TLE-compliant data models. The process is engineered for reproducibility and for validating the methodology’s core claims. The complete, step-bystep implementation details are available for inspection and verification in Appendix A.17. Process Flow (high level) 1. Frontend — Visitor entry & pattern selection: The frontend collects visitor data, including each party’s initial pattern choices. 2. Backend — Dynamic generation: The Locations table is consulted to deterministically generate TLE tables (CREATE TABLE statements). 3. UI — Shared rendering: A single Razor view and ViewModel are reused across levels to render pattern options, reducing duplication. 4. Data update — Bitmask write: User actions are persisted by updating the bitmask column in the grandparent table (typically a single-row O(1) operation). Key Methodology Claims (Instantiated in the MVP) • Hierarchy-Aware Design: Logical table boundaries are enforced for each threelevel scope via TLE, aligning with structured decomposition principles in hierarchical relational schemas [118]. • Bitmask Optimization: Compact selection encoding enables constant-time set, clear, and test operations using native bitwise expressions in SQL Server, reflecting established practices in encoded and columnar data representations [23,53,55,118]. • Reusable Workflow: A single MVC controller and ViewModel operate across all hierarchical levels, minimizing ORM complexity and duplication in line with multi-view reuse patterns in enterprise MVC frameworks [142]. 152 of 186 • Bounded Refinement: Refinement steps are capped at Rₘₐₓ = 50 per level, as defined in Table 42, enforcing loop bounds consistent with formal lifecycledriven termination strategies [83]. • Exceeding Rₘₐₓ transitions the workflow to state S8, as specified in Table A.14.2, enforcing bounded iteration and controlled bailout paths consistent with ISO/IEC 12207 lifecycle termination principles [87]. A.14.11 Key Claims Supported and Academic Grounding This MVP provides empirical evidence supporting the following claims, grounded in established computer science and database literature (See Table A.14.8). Table A.14.8. Key Claims Supported and Academic Grounding Claim Academic Grounding Bitwise/encoded access provides substantial read efficiency for pattern queries. Grounded in columnar/encoding database literature [23,53,55] Recursive-CTE/adjacency-list traversal has depth-dependent costs (worse for broad/deep hierarchies). Grounded in classical database texts on hierarchical representations and relational trade-offs [118] TLE’s dynamic table approach is a practical denormalization strategy that trades schema complexity for query and operational efficiency. Consistent with schema evolution and polyglot persistence research [90] Bounded iterative refinement and backtracking map to classical search/backtracking techniques. Supported by DFS/BFS algorithmic foundations and process-refinement literature [62,77,83] Formal verification of workflow/state-machine behavior aligns with CSP paradigms, and the MVP inherits its structural and behavioral guarantees from the verified Generic model. Grounded in process algebra and model checking guidance (CSP) [45, 71, 87], as applied to the Generic model from which the MVP is derived By integrating these elements, the PBFD MVP operationalizes concepts typically treated in isolation—encoded storage, bounded search, hierarchical partitioning, and verification—into a unified and reproducible development methodology. A.15 PBFD MVP State Machine Workflow Mermaid Code Mermaid Code for Figure A.14.2: stateDiagram-v2 direction TB [*] --> S0 state "S0: Level 1<br>Process/Validate/Resolve<br>(TLE 1–3)" as S0 state "S1: Level 2<br>Process/Validate/Resolve<br>(TLE 2–4)" as S1 state "S2: Level 3<br>Process/Validate/Resolve<br>(TLE 3–5)" as S2 state "S3: Level 4<br>Process/Validate/Resolve<br>(TLE 4–6)" as S3 state "S4: Level 5<br>Process/Validate<br>(TLE 5–7)" as S4 state "S5: Refine L1-L3" as S5 state "S6: Finalize All" as S6 state "S7: Complete" as S7 state "S8: Error" as S8 S0 --> S1 : PBFD2<br>S0 done S1 --> S2 : PBFD3<br>S1 done S2 --> S3 : PBFD4<br>S2 done S3 --> S4 : PBFD5<br>S3 done 153 of 186 S2 --> S5 : PBFD6<br>S2 fail S5 --> S0 : PBFD7<br>Refined S5 --> S8 : PBFD8<br>Attempts≥50 S4 --> S6 : PBFD9<br>S4 done S6 --> S7 : PBFD10<br>Complete S7 --> [*] A.16 Quantifying Node Reduction in Perfect N-ary Trees This section quantifies the number of nodes remaining in a perfect n-ary tree after removing all leaves (nodes at the deepest level) and their immediate parent nodes. We assume a perfect n-ary tree of height h, where all levels are fully filled. Key Formula • Total Nodes (before removal): ∑𝑛𝑘 ℎ 𝑘=0 =𝑛(ℎ+1)−1 𝑛−1 • Nodes removed: o Leaves (level h): 𝑛ℎ nodes o Parent level (level h−1): 𝑛(ℎ−1) nodes • Remaining nodes (after removing leaves and their parents): 𝑁𝑟𝑒𝑚𝑎𝑖𝑛𝑖𝑛𝑔 = 𝑁𝑡𝑜𝑡𝑎𝑙 −(𝑛ℎ+𝑛(ℎ−1))=𝑛(ℎ+1)−1 𝑛−1 −(𝑛ℎ+𝑛(ℎ−1)) Remaining Nodes (after removing leaves and their parents): 𝑃𝑟𝑒𝑚𝑎𝑖𝑛𝑖𝑛𝑔 =(𝑁𝑟𝑒𝑚𝑎𝑖𝑛𝑖𝑛𝑔 𝑁𝑡𝑜𝑡𝑎𝑙 )×100% Example: Ternary Tree (n = 3) of Height h = 6 Step 1: Compute the Total Nodes 𝑁𝑡𝑜𝑡𝑎𝑙 =3(6+1)−1 3−1 =3(7)−1 2=2187−1 2=1093 nodes Step 2: Compute the Nodes to Remove • Leaves (Level 6): 36=729 nodes • Parent Level (Level 5): 35=243 nodes • Total Nodes Removed: 729+243 =972 nodes Step 3: Compute the Remaining Nodes 𝑁𝑟𝑒𝑚𝑎𝑖𝑛𝑖𝑛𝑔 = 1093 − 972 = 121 nodes Step 4: Compute the Remaining Nodes’ Percentage 𝑃𝑟𝑒𝑚𝑎𝑖𝑛𝑖𝑛𝑔 =121 1093×100% ≈11.07% Step 5: Percentage of Last Two Levels o Nodes in last two levels: 729 + 243 = 972 nodes o Percentage of last two levels: (972 / 1093) × 100% ≈ 88.93% Thus, after removing the leaves and their parent level, only 121 nodes or approximately 11% remain in the tree. The last two levels (5 and 6) constitute approximately 89% of the total tree (see Table A.16.1). Table A.16.1. Summary for Ternary Tree (n = 3, h = 6) Metric Value Percentage Total nodes 1,093 100.00%