Case Study: Enhancing GAMP CSV Lifecycle with Axiomatic Semantics for Validating 32 Karat Software

Historical Scenario: Alpha Life Sciences and the 32 Karat Software Integration for a global Contract Research, Development and Manufacturing Organization (CRDMO) offering end-to-end solutions that enable partners to discover, develop and manufacture biologics

Introduction

In a groundbreaking collaboration, Alpha Life Sciences Ltd. embarked on a transformative journey. Our mission? Develop, CSV validate for DI requirements, and unveil a cutting-edge Quality Control (QC) lab equipped with the revolutionary 32 Karat Software for the PA 800 system. This case study chronicles how Axiomatic Semantics, a formal method for specifying and verifying software behavior, elevated the GAMP CSV lifecycle to new heights. The outcome: a robust validation of the 32 Karat Software that not only met but exceeded stringent Data Integrity (DI) requirements.

Step 1: Requirements Analysis and Functional Specification

1.1 Identifying Stakeholders

A cross-functional team united chromatography experts, software developers, quality assurance personnel, and regulatory officers. This assembly ensured the full spectrum of perspectives in the requirements gathering process.

1.2 Collecting Requirements

Workshops and interviews provided the foundation for a diverse array of requirements, encompassing both the functional and non-functional realms. Notably, a pivotal user requirement emerged: "Data must be stored in a secure format."

1.3 Documenting Requirements

The team harnessed the SMART criteria to convert requirements into precise and unequivocal statements. This translation process crystallized high-level goals into actionable directives.

1.4 Formulating Functional Specification

Detailed functional specifications emerged, meticulously charting the behavior of the 32 Karat Software. Inputs, processing steps, outputs, and interactions formed a comprehensive blueprint.

1.5 Axiomatic Semantics Perspective

Each requirement, including the critical "Data must be stored in a secure format," underwent translation into formal properties utilizing the notation of Axiomatic Semantics. These formal properties established the bedrock for subsequent validation.

Formal Property

For all data instances D and formats F, S(D, F) ? SecureFormat(D, F)

Explanation: ? D, F : If data instance D is stored in format F, then it adheres to the SecureFormat property.

Step 2: Deriving Formal Properties

2.1 Mapping Requirements to Properties

Through the prism of Axiomatic Semantics, each requirement seamlessly converged with a corresponding formal property. This confluence was achieved by expressing the requirement within a logical framework.

Example (Requirement): "Data must be stored in a secure format."

Axiomatic Semantics Formal Property: ?D,F:S(D,F)

Where:

• D embodies all possible data instances.
• F represents all conceivable format instances.
• S(D,F) signifies the secure storage of data D within format F.

Benefits of Axiomatic Semantics Integration

Enhanced Precision: Axiomatic Semantics empowered Alpha Life Sciences to delineate user requirements with mathematical precision, ensuring alignment with intended software behavior.

Regulatory Compliance: By crystallizing requirements using formal notation, Alpha Life Sciences demonstrated that user requirements flawlessly metamorphosed into formal properties, thus mitigating potential compliance concerns.

Step 3: Model Specification and Verification

3.1 Creating Labeled Transition System (LTS)

Crucial to the validation of the 32 Karat Software within the compliance ambit was the accurate modeling of its behavior. This is where the Labeled Transition System (LTS) played a pivotal role. The LTS, a formal representation, adeptly encapsulated the software's behaviors that are relevant to the data integrity / compliance / security of the system, through states, transitions, and actions.

Example Scenario: Data Storage in Secure Format

States (S):

1. Initial State: Software initialized and ready to accept data.
2. Data Entry: Data is being entered into the system.
3. Data Storage: Data is stored in the system after entry.
4. Compliance Check: The system performs compliance checks on stored data.
5. Secure Storage: Data is securely stored in compliance with the SecureFormat property.

Transitions (T):

• Transition from Initial to Data Entry state when data is input.
• Transition from Data Entry to Data Storage state when data is submitted.
• Transition from Data Storage to Compliance Check state after successful storage.
• Transition from Compliance Check to Secure Storage state after compliance is confirmed.

Actions (A):

• Input Data: Action representing the input of data.
• Submit Data: Action representing the submission of data.
• Check Compliance: Action representing compliance checks.
• Store Securely: Action representing secure data storage.

LTS Diagram:

Initial State (S1) ? Data Entry (S2) [Input Data] ? Data Storage (S3) [Submit Data] ? Compliance Check (S4) [Check Compliance] ? Secure Storage (S5) [Store Securely]

3.2 Defining Axiomatic Semantics Properties

To ensure unwavering data integrity and compliance, formal properties birthed from Axiomatic Semantics were seamlessly interwoven into the LTS model. Consider the formal property linked to the "Data must be stored in a secure format" requirement:

Formal Property:

For all data instances D and formats F, S(D, F) ? SecureFormat(D, F)

Verification through Manual Verification of LTS Model

In the absence of automated "Model Checker" tools, a more hands-on approach was chosen. Post the creation of the labeled transition system (LTS) model for the 32 Karat Software, the next step involved manual verification of formal properties. Given the constraints of unavailable software-based model verification tools, manual verification proved effective, particularly within the scope of data integrity, compliance, and security.

3.2.1 Reviewing LTS with Formal Properties

We methodically scrutinized the LTS model, focusing on states, transitions, and actions that are relevant to the data integrity / compliance / security of the system. We ensured that the LTS precisely mirrored the software's behavior, particularly within the context of data integrity, compliance, and security.

3.2.2 Manual Verification of Formal Properties

For each formal property derived from Axiomatic Semantics, we subjected it to rigorous manual verification within the LTS model.

Example (Formal Property): Data must be stored in a secure format.

1. Identify states in the LTS model where data storage or manipulation takes place. These states may entail data transmission, storage, or retrieval.
2. Analyze transitions between states to grasp how data is processed and stored.
3. Examine the formal property ? D, F : S(D, F). In this context, it signifies that for all data instances D and storage formats F, the software guarantees secure storage.
4. Trace transitions linked to data storage in the LTS model. Evaluate whether the storage format (F) conforms to the security requisites outlined in the formal property.
5. If the software employs encryption or access controls for secure data storage, ascertain the LTS model accurately reflects these mechanisms.

Benefits of Manual Verification

Although manual verification demanded more time compared to software-based model checking, it delivered a range of advantages:

• Customization: Manual verification could be tailored to the software's scope and requirements (DI/Compliance/Security).
• Comprehensive Insight: We closely inspected the LTS model, transitions, and states for a profound grasp of the software's behavior within the defined scope.
• Flexibility: We tailored the manual verification process to available resources and the system's complexity.
• Enhanced Understanding: Manual verification deepened our understanding of the software's behavior and alignment with formal properties.

Note: We documented the manual verification process meticulously, including steps taken, outcomes, and observations linked to data integrity, compliance, and security to be used as input into the GAMP lifecycle documents.

By manually verifying the LTS model against formal properties, we guaranteed the 32 Karat Software meets data integrity, compliance, and security requirements within the system's scope. This approach underscores Alpha Life Sciences' commitment to precision, quality, and regulatory excellence, even in the absence of software-based model checking tools.

Step 4: Test Protocol Development

4.1 Creating Test Cases

Test cases were formulated based on formal properties and LTS models. Notably, the property "Data must be stored in a secure format" steered the creation of specific test cases.

4.2 Defining Inputs and Expected Outputs

Inputs, anticipated outputs, and actions were precisely defined for each test case. The SecureFormat property guided the construction of pertinent tests.

Example (Property):

Test Case: Validate that data stored in format F adheres to SecureFormat property.

Steps:

1. Input data instance D and format F.
2. Observe system behavior.
3. Verify satisfaction of SecureFormat(D, F) property.

Step 5: Execution and Analysis

5.1 Executing Test Cases

Test cases were rigorously executed on the 32 Karat Software using real-world data instances and formats.

5.2 Comparing Results

Results were meticulously juxtaposed with expected outcomes based on formal properties. The SecureFormat property ensured data integrity and security.

Step 6: Documentation and Reporting

6.1 Results Compilation

Comprehensive documentation of test case execution results ensued, cataloging successes, inconsistencies, and deviations.

6.2 Deviation Analysis

Deviation analysis dissected inconsistencies vis-à-vis the SecureFormat property. The impact on data integrity and security was methodically assessed.

6.3 Corrective Actions

In case of deviations, a partnership with vendors was forged to remedy issues. Subsequent re-testing assured compliance.

Step 7: Integration with CSV Lifecycle

7.1 Requirements Analysis

Integration into the GAMP CSV lifecycle unfolded seamlessly. Each requirement seamlessly corresponded to an applicable formal property.

7.2 Risk Assessment

In the context of the ERES assessment, risks/gaps stemming from deviations of formal properties were evaluated. Impacts on data integrity and security were meticulously weighed.

7.3 Validation Closure

Validation closure necessitated the confirmation of all formal properties. The SecureFormat property, for instance, cemented data security.

Conclusion

The voyage of fortifying the GAMP CSV lifecycle through Axiomatic Semantics for validating the 32 Karat Software showcased Alpha Life Sciences' steadfast dedication to precision and quality. The formal properties birthed from Axiomatic Semantics served as a robust scaffold for validating critical software behavior, fortifying data integrity, and harmonizing with regulatory benchmarks. This historical case study serves as a testament to how a methodical approach can redefine validation practices and enhance data security within the QC lab milieu.