Add SpeckDL examples with Dark Provenance primitives
This commit is contained in:
Scott Scoble
parent
9bcbb3d77c
commit
712ec94495
5 changed files with 648 additions and 0 deletions
157
examples/AccessControl.speck
Normal file
157
examples/AccessControl.speck
Normal file
|
|
@ -0,0 +1,157 @@
|
|||
// AccessControl.speck
|
||||
// Derives/satisfies for regulatory traceability
|
||||
//
|
||||
// Provenance: Access control system requiring full regulatory
|
||||
// compliance traceability. Every access decision must be traceable
|
||||
// to its source requirements and regulatory clauses.
|
||||
//
|
||||
// SpeckBOM: Full BOM with regulatory traceability, audit
|
||||
// logging requirements, and compliance verification.
|
||||
//
|
||||
// Author: Security Engineering Team <security@scoble.me>
|
||||
// Source: Security Architecture Review, SOC 2 Compliance Audit
|
||||
|
||||
speck AccessControl {
|
||||
// SpeckBOM - declare toolchain and compliance metadata
|
||||
bom {
|
||||
compiler: "speckl-compile" version "0.2.0"
|
||||
solver: "z3" version "4.12.5"
|
||||
runtime: "wasm-runtime" version "1.0.0"
|
||||
license: "MIT"
|
||||
hash: "sha256: AccessControl-base-v1"
|
||||
}
|
||||
|
||||
// Intent provenance - regulatory and security context
|
||||
provenance {
|
||||
regulation: "SOC 2 Type II" // Trust Services Criteria
|
||||
regulation: "ISO 27001:2022" // Information security
|
||||
regulation: "GDPR Article 32" // Security of processing
|
||||
design_decision: "ADR-0012 Identity and Access Management"
|
||||
parent_spec: "SecurityFoundation"
|
||||
external_doc: "NIST SP 800-63B" at "https://pages.nist.gov/800-63-3/sp800-63b.html"
|
||||
}
|
||||
|
||||
// Traceability to security requirements and regulatory clauses
|
||||
satisfies ACCESS-REQ-001
|
||||
satisfies ACCESS-REQ-002 clause "4.1.3"
|
||||
satisfies ACCESS-REQ-003 clause "5.2.1"
|
||||
satisfies SOC2-CC-6-1 clause "Logical access security"
|
||||
satisfies SOC2-CC-7-1 clause "Security monitoring"
|
||||
satisfies GDPR-ART-32 clause "Security of processing"
|
||||
|
||||
// Authorship and origin
|
||||
author: "Security Engineering" <"security@scoble.me">
|
||||
source: architecture_review ref "AR-2024-0108"
|
||||
source: compliance_audit ref "AUDIT-2024-SOC2-001"
|
||||
source: meeting ref "zoom://2024-01-15/security-architecture"
|
||||
|
||||
// Verification boundary - manual review required for security changes
|
||||
review: manual
|
||||
|
||||
// Derives from security foundation, satisfies access control requirements
|
||||
derives from SecurityFoundation via "access control policy enforcement"
|
||||
satisfies SECURITY-REQ-001
|
||||
|
||||
// Input: access request and context
|
||||
input: {
|
||||
userId: String,
|
||||
resourceId: String,
|
||||
requestedAction: Action,
|
||||
userRoles: [String],
|
||||
userGroups: [String],
|
||||
timestamp: Nat,
|
||||
ipAddress: String,
|
||||
deviceFingerprint: String,
|
||||
sessionToken: String
|
||||
}
|
||||
|
||||
// Output: access decision and metadata
|
||||
output: {
|
||||
allowed: Bool,
|
||||
reason: String,
|
||||
policyId: String,
|
||||
auditTrail: [String],
|
||||
rateLimitRemaining: Nat,
|
||||
sessionValid: Bool
|
||||
}
|
||||
|
||||
// Constraints - access control invariants
|
||||
constraint: userId != ""
|
||||
constraint: resourceId != ""
|
||||
constraint: timestamp > 0
|
||||
constraint: count(userRoles) >= 0
|
||||
constraint: count(userGroups) >= 0
|
||||
constraint: sessionToken != ""
|
||||
|
||||
// Policy constraints - must have valid policy
|
||||
constraint: policyId != ""
|
||||
constraint: implies(allowed, policyId != "")
|
||||
constraint: implies(not allowed, reason != "")
|
||||
|
||||
// Rate limiting constraint
|
||||
constraint: rateLimitRemaining >= 0
|
||||
constraint: rateLimitRemaining <= 100
|
||||
|
||||
// Session validation constraint
|
||||
constraint: implies(sessionValid, sessionToken != "")
|
||||
|
||||
// Verification: access decisions are correct
|
||||
verify: always(implies(
|
||||
allowed,
|
||||
hasPermission(userId, resourceId, requestedAction, userRoles, userGroups)
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
not allowed,
|
||||
not hasPermission(userId, resourceId, requestedAction, userRoles, userGroups)
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
rateLimitRemaining == 0,
|
||||
allowed == false
|
||||
))
|
||||
|
||||
// Verification: audit trail is complete
|
||||
verify: always(implies(
|
||||
allowed or not allowed,
|
||||
count(auditTrail) >= 1
|
||||
))
|
||||
|
||||
// Events for security audit trail
|
||||
event AccessAttempt {
|
||||
userId: String
|
||||
resourceId: String
|
||||
requestedAction: String
|
||||
allowed: Bool
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event AccessDenied {
|
||||
userId: String
|
||||
resourceId: String
|
||||
requestedAction: String
|
||||
reason: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event PolicyEvaluated {
|
||||
policyId: String
|
||||
userId: String
|
||||
resourceId: String
|
||||
result: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event RateLimited {
|
||||
userId: String
|
||||
requestCount: Nat
|
||||
limit: Nat
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event SessionInvalidated {
|
||||
sessionToken: String
|
||||
reason: String
|
||||
timestamp: Nat
|
||||
}
|
||||
}
|
||||
119
examples/DrugDosageCalculator.speck
Normal file
119
examples/DrugDosageCalculator.speck
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
// DrugDosageCalculator.speck
|
||||
// Medical device showing provenance + SpeckBOM annotations
|
||||
//
|
||||
// Provenance: This is a safety-critical medical device component.
|
||||
// Every calculation must be traceable to regulatory requirements,
|
||||
// design decisions, and clinical evidence.
|
||||
//
|
||||
// SpeckBOM: Full bill of materials including compiler, solver,
|
||||
// runtime, and full provenance graph with regulatory traceability.
|
||||
//
|
||||
// Author: Dr. Sarah Chen <s.chen@meddevice.example>
|
||||
// Source: IEC 62304 Class C medical device standard
|
||||
|
||||
speck DrugDosageCalculator {
|
||||
// SpeckBOM - critical for medical device compliance
|
||||
bom {
|
||||
compiler: "speckl-compile" version "0.2.0"
|
||||
solver: "z3" version "4.12.5"
|
||||
runtime: "wasm-runtime" version "1.0.0"
|
||||
license: "MIT"
|
||||
hash: "sha256: DrugDosageCalculator-base-v1"
|
||||
}
|
||||
|
||||
// Intent provenance - regulatory and design context
|
||||
provenance {
|
||||
regulation: "FDA 21 CFR 820.30" // Quality system regulation
|
||||
regulation: "IEC 62304 Class C" // Medical device software lifecycle
|
||||
regulation: "ISO 14971" // Risk management
|
||||
design_decision: "ADR-0023 Infusion Safety Architecture"
|
||||
external_doc: "AAMI TIR32" at "https://www.aami.org/tir32"
|
||||
parent_spec: "InfusionPumpBase" // Decomposition
|
||||
}
|
||||
|
||||
// Traceability to system requirements and regulatory clauses
|
||||
satisfies SYS-REQ-042
|
||||
satisfies SYS-REQ-043 clause "5.2.1"
|
||||
satisfies FDA-820-30 clause "d"
|
||||
satisfies IEC-62304-Annex-3
|
||||
|
||||
// Authorship and origin
|
||||
author: "Dr. Sarah Chen" <"s.chen@meddevice.example">
|
||||
source: architecture_review ref "AR-2024-0315"
|
||||
source: meeting ref "zoom://2024-03-10/medical-device-wg"
|
||||
|
||||
// Verification boundary - MANUAL REVIEW REQUIRED before deployment
|
||||
review: manual
|
||||
|
||||
// Parent spec relationship - decomposed from broader controller
|
||||
derives from InfusionPumpController via "decomposition of dosing logic"
|
||||
|
||||
// Input parameters for dosage calculation
|
||||
input: {
|
||||
patientWeight: Real, // Patient weight in kg
|
||||
drugConcentration: Real, // Drug concentration (mg/mL)
|
||||
prescribedDose: Real, // Prescribed dose (mg)
|
||||
minDose: Real, // Minimum therapeutic dose (mg)
|
||||
maxDose: Real, // Maximum safe dose (mg)
|
||||
frequency: Nat, // Administration frequency (times/day)
|
||||
vtbi: Real // Volume to be infused (mL)
|
||||
}
|
||||
|
||||
// Output: calculated dosage and safety flags
|
||||
output: {
|
||||
volume: Real, // Calculated volume (mL)
|
||||
safe: Bool, // Safety flag
|
||||
concentrationCheck: Bool, // Concentration within limits
|
||||
weightBasedCheck: Bool, // Weight-based calculation validated
|
||||
maxRateCheck: Bool // Rate within safe limits
|
||||
}
|
||||
|
||||
// Safety constraints - ALL must hold for valid dosage
|
||||
constraint: patientWeight > 0
|
||||
constraint: patientWeight <= 200 // Max realistic patient weight
|
||||
constraint: drugConcentration > 0
|
||||
constraint: drugConcentration <= 100 // Realistic concentration range
|
||||
constraint: minDose > 0
|
||||
constraint: maxDose > minDose
|
||||
constraint: frequency >= 1
|
||||
constraint: frequency <= 6 // Reasonable frequency limits
|
||||
constraint: vtbi > 0
|
||||
constraint: vtbi <= 1000 // Typical IV bag sizes
|
||||
|
||||
// Therapeutic constraints - dose must be clinically appropriate
|
||||
constraint: implies(safe, volume >= minDose / drugConcentration)
|
||||
constraint: implies(safe, volume <= maxDose / drugConcentration)
|
||||
constraint: implies(not safe, volume == 0) // No dose if unsafe
|
||||
|
||||
// Safety verification - critical properties that must be proven
|
||||
verify: always(implies(
|
||||
prescribedDose >= minDose and prescribedDose <= maxDose,
|
||||
safe
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
patientWeight <= 0 or drugConcentration <= 0,
|
||||
not safe
|
||||
))
|
||||
|
||||
verify: always(implies(not safe, volume == 0))
|
||||
|
||||
// Events for clinical traceability and audit
|
||||
event DoseCalculated {
|
||||
volume: Real
|
||||
safe: Bool
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event DoseRejected {
|
||||
reason: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event CriticalLimitExceeded {
|
||||
parameter: String
|
||||
value: Real
|
||||
limit: Real
|
||||
timestamp: Nat
|
||||
}
|
||||
}
|
||||
143
examples/PaymentService.speck
Normal file
143
examples/PaymentService.speck
Normal file
|
|
@ -0,0 +1,143 @@
|
|||
// PaymentService.speck
|
||||
// Import pinning with hash verification
|
||||
//
|
||||
// Provenance: Payment processing system component requiring strict
|
||||
// integrity verification of all dependencies. Import hashes ensure
|
||||
// reproducibility and tamper detection.
|
||||
//
|
||||
// SpeckBOM: Full BOM with import pinning, compiler versions, and
|
||||
// hash verification for all transitive dependencies.
|
||||
//
|
||||
// Author: Platform Engineering Team <platform@scoble.me>
|
||||
// Source: Payment Systems Architecture Review, PCI-DSS Compliance Audit
|
||||
|
||||
speck PaymentService {
|
||||
// SpeckBOM - declare toolchain with version pinning
|
||||
bom {
|
||||
compiler: "speckl-compile" version "0.2.0"
|
||||
solver: "z3" version "4.12.5"
|
||||
runtime: "wasm-runtime" version "1.0.0"
|
||||
license: "MIT"
|
||||
hash: "sha256: PaymentService-base-v1"
|
||||
}
|
||||
|
||||
// Intent provenance - regulatory and architectural context
|
||||
provenance {
|
||||
regulation: "PCI-DSS v4.0 Requirement 6.1" // Secure coding standards
|
||||
regulation: "PCI-DSS v4.0 Requirement 6.3" // Change management
|
||||
regulation: "PCI-DSS v4.0 Requirement 10.1" // Audit logging
|
||||
design_decision: "ADR-0035 Payment Gateway Strategy"
|
||||
parent_spec: "TransactionProcessor"
|
||||
external_doc: "OWASP Payment Handling Guidelines" at "https://owasp.org/payment"
|
||||
}
|
||||
|
||||
// Traceability to system requirements and compliance
|
||||
satisfies PAYMENT-REQ-001
|
||||
satisfies PAYMENT-REQ-002 clause "4.2.1"
|
||||
satisfies PCI-DSS-6-1 clause "Secure coding practices"
|
||||
satisfies PCI-DSS-10-1 clause "Audit trails"
|
||||
|
||||
// Authorship and origin
|
||||
author: "Platform Engineering" <"platform@scoble.me">
|
||||
source: architecture_review ref "AR-2024-0410"
|
||||
source: compliance_audit ref "AUDIT-2024-Q2-PAYMENT"
|
||||
|
||||
// Verification boundary - automated with spot-check sampling
|
||||
review: hybrid
|
||||
|
||||
// Derives from payment processor base, satisfies transaction requirements
|
||||
derives from TransactionProcessor via "specialization for payment operations"
|
||||
satisfies TRANSACTION-REQ-001
|
||||
|
||||
// Import statements with version pinning and hash verification
|
||||
// These imports must match exactly - hash checked at compile time
|
||||
import "rate-limiter.speck" as limiter
|
||||
hash: "sha256:f7a1b2c3d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1"
|
||||
version: "2.1.0"
|
||||
|
||||
import "retry-handler.speck" as retry
|
||||
hash: "sha256:b3c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1b2c3"
|
||||
version: "1.4.0"
|
||||
|
||||
import "fraud-scanner.speck" as fraud
|
||||
hash: "sha256:a1b2c3d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1b2c3"
|
||||
version: "3.0.0"
|
||||
|
||||
// Input parameters for payment processing
|
||||
input: {
|
||||
payment: Payment,
|
||||
apiKey: String,
|
||||
merchantId: String,
|
||||
customerIp: String,
|
||||
userAgent: String
|
||||
}
|
||||
|
||||
// Output: processing result and metadata
|
||||
output: {
|
||||
result: PaymentResult,
|
||||
transactionId: String,
|
||||
fraudScore: Real,
|
||||
fraudFlags: [String],
|
||||
rateLimitRemaining: Nat,
|
||||
retryCount: Nat
|
||||
}
|
||||
|
||||
// Constraints - payment processing invariants
|
||||
constraint: limiter.maxRequests == 100
|
||||
constraint: limiter.window == 60
|
||||
constraint: retry.maxRetries == 3
|
||||
constraint: fraud.fraudCheckEnabled == true
|
||||
constraint: transactionId != ""
|
||||
|
||||
// Rate limiting constraint
|
||||
constraint: implies(not limiter.allowed, result == RateLimited)
|
||||
|
||||
// Retry constraint - if rate limited, must retry with backoff
|
||||
constraint: implies(result == RateLimited, retryCount > 0)
|
||||
|
||||
// Fraud constraint - fraud score must be calculated
|
||||
constraint: fraudScore >= 0
|
||||
constraint: fraudScore <= 100
|
||||
|
||||
// Verify: rate limiting works correctly
|
||||
verify: always(implies(
|
||||
limiter.remaining == 0,
|
||||
result == RateLimited
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
result == Success,
|
||||
transactionId != ""
|
||||
))
|
||||
|
||||
// Events for payment audit trail
|
||||
event PaymentProcessed {
|
||||
transactionId: String
|
||||
amount: Real
|
||||
currency: String
|
||||
status: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event RateLimited {
|
||||
clientIp: String
|
||||
requestCount: Nat
|
||||
windowSeconds: Nat
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event FraudDetected {
|
||||
transactionId: String
|
||||
fraudScore: Real
|
||||
flags: [String]
|
||||
action: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event RetryAttempted {
|
||||
transactionId: String
|
||||
attemptNumber: Nat
|
||||
delayMs: Nat
|
||||
timestamp: Nat
|
||||
}
|
||||
}
|
||||
91
examples/RetryHandler.speck
Normal file
91
examples/RetryHandler.speck
Normal file
|
|
@ -0,0 +1,91 @@
|
|||
// RetryHandler.speck
|
||||
// Simple retry with backoff constraints
|
||||
//
|
||||
// Provenance: This spec defines a standard retry mechanism used across
|
||||
// multiple services. It's a foundational component for resilience patterns.
|
||||
//
|
||||
// BOM: This spec is version-pinned and hash-verified for reproducibility.
|
||||
//
|
||||
// Author: Scott Scoble <scott@scoble.me>
|
||||
// Source: Architecture review ADR-0021 - Resilience Patterns
|
||||
|
||||
speck RetryHandler {
|
||||
// SpeckBOM - declare toolchain dependencies and integrity
|
||||
bom {
|
||||
compiler: "speckl-compile" version "0.2.0"
|
||||
solver: "z3" version "4.12.5"
|
||||
runtime: "wasm-runtime" version "1.0.0"
|
||||
license: "MIT"
|
||||
hash: "sha256: RetryHandler-base-v1"
|
||||
}
|
||||
|
||||
// Intent provenance - where did this spec come from?
|
||||
provenance {
|
||||
design_decision: "ADR-0021 Resilience Patterns"
|
||||
external_doc: "AWS Retry Best Practices" at "https://aws.amazon.com/architecture/retry/"
|
||||
}
|
||||
|
||||
// Traceability - derives from base fault handler, satisfies resiliency requirements
|
||||
derives from FaultHandler via "specialization for retry logic"
|
||||
satisfies RESILIENCE-REQ-01 clause "3.1.2"
|
||||
satisfies RESILIENCE-REQ-02
|
||||
|
||||
// Who wrote this and why
|
||||
author: "Scott Scoble" <"scott@scoble.me">
|
||||
source: architecture_review ref "AR-2024-0215"
|
||||
|
||||
// Verification boundary - this needs manual review
|
||||
review: manual
|
||||
|
||||
// Input: operation to retry, max retries allowed
|
||||
input: {
|
||||
operation: Operation,
|
||||
maxRetries: Nat,
|
||||
initialDelay: Real,
|
||||
maxDelay: Real
|
||||
}
|
||||
|
||||
// Output: result of operation (success or final failure)
|
||||
output: {
|
||||
success: Bool,
|
||||
finalResult: String,
|
||||
attemptCount: Nat,
|
||||
totalDelay: Real
|
||||
}
|
||||
|
||||
// Constraints - invariants that must hold
|
||||
constraint: maxRetries <= 10
|
||||
constraint: maxRetries >= 0
|
||||
constraint: initialDelay > 0
|
||||
constraint: maxDelay >= initialDelay
|
||||
constraint: totalDelay == sum(delays)
|
||||
constraint: totalDelay <= 30s
|
||||
|
||||
// Backoff constraint - delay grows exponentially
|
||||
constraint: backoff(delay(n)) == delay(n-1) * 2
|
||||
constraint: delay(n) <= maxDelay
|
||||
|
||||
// Verify: if retry attempt > 1, delay must be positive
|
||||
verify: always(implies(attempt > 1, delay > 0))
|
||||
|
||||
// Verify: if all retries exhausted, operation must have failed
|
||||
verify: always(implies(attemptCount == maxRetries + 1, not success))
|
||||
|
||||
// Events for observability and provenance tracking
|
||||
event RetryAttempted {
|
||||
attemptNumber: Nat
|
||||
delay: Real
|
||||
remainingRetries: Nat
|
||||
}
|
||||
|
||||
event OperationSucceeded {
|
||||
attemptCount: Nat
|
||||
totalDelay: Real
|
||||
}
|
||||
|
||||
event OperationFailed {
|
||||
attemptCount: Nat
|
||||
totalDelay: Real
|
||||
finalError: String
|
||||
}
|
||||
}
|
||||
138
examples/TemperatureMonitor.speck
Normal file
138
examples/TemperatureMonitor.speck
Normal file
|
|
@ -0,0 +1,138 @@
|
|||
// TemperatureMonitor.speck
|
||||
// IoT with constraint-based verification
|
||||
//
|
||||
// Provenance: IoT sensor monitoring system for industrial safety.
|
||||
// All temperature readings must be verified against safety constraints
|
||||
// before triggering alerts or actions.
|
||||
//
|
||||
// SpeckBOM: Full BOM including sensor firmware hashes and
|
||||
// constraint verification results for compliance.
|
||||
//
|
||||
// Author: Industrial IoT Team <iot@scoble.me>
|
||||
// Source: Safety Critical Systems Design Review, ISO 13849 Compliance
|
||||
|
||||
speck TemperatureMonitor {
|
||||
// SpeckBOM - declare toolchain and firmware hashes
|
||||
bom {
|
||||
compiler: "speckl-compile" version "0.2.0"
|
||||
solver: "z3" version "4.12.5"
|
||||
runtime: "wasm-runtime" version "1.0.0"
|
||||
license: "MIT"
|
||||
hash: "sha256: TemperatureMonitor-base-v1"
|
||||
}
|
||||
|
||||
// Intent provenance - safety and compliance context
|
||||
provenance {
|
||||
regulation: "ISO 13849" // Machinery safety
|
||||
regulation: "IEC 62061" // Functional safety
|
||||
design_decision: "ADR-0048 Industrial IoT Architecture"
|
||||
external_doc: "ISO 13849-2:2015 Annex B" at "https://www.iso.org/standard/59384.html"
|
||||
external_doc: "IEC 62061:2021" at "https://www.iec.ch/dynamic/publication/62061"
|
||||
}
|
||||
|
||||
// Traceability to safety requirements
|
||||
satisfies SAFETY-REQ-001
|
||||
satisfies SAFETY-REQ-002 clause "5.3.1"
|
||||
satisfies ISO-13849-5 clause "Performance Level requirements"
|
||||
|
||||
// Authorship and origin
|
||||
author: "Industrial IoT Team" <"iot@scoble.me">
|
||||
source: architecture_review ref "AR-2024-0520"
|
||||
source: compliance_audit ref "AUDIT-2024-INDUSTRY-001"
|
||||
|
||||
// Verification boundary - automatic verification for sensor data
|
||||
review: auto
|
||||
|
||||
// Derives from sensor base, satisfies safety requirements
|
||||
derives from SensorMonitor via "temperature-specific monitoring logic"
|
||||
satisfies SENSOR-REQ-001
|
||||
|
||||
// Input: sensor readings and configuration
|
||||
input: {
|
||||
currentTemp: Real, // Current temperature reading (°C)
|
||||
ambientTemp: Real, // Ambient temperature (°C)
|
||||
setPoint: Real, // Target temperature (°C)
|
||||
maxTemp: Real, // Maximum safe temperature (°C)
|
||||
minTemp: Real, // Minimum safe temperature (°C)
|
||||
hysteresis: Real, // Hysteresis band (°C)
|
||||
sensorId: String, // Sensor identifier
|
||||
calibrationOffset: Real // Calibration offset (°C)
|
||||
}
|
||||
|
||||
// Output: monitoring result and actions
|
||||
output: {
|
||||
status: TempStatus,
|
||||
alert: Bool,
|
||||
action: TempAction,
|
||||
safe: Bool,
|
||||
deviation: Real,
|
||||
timeInAlert: Real
|
||||
}
|
||||
|
||||
// Constraints - temperature safety invariants
|
||||
constraint: maxTemp > setPoint
|
||||
constraint: setPoint > minTemp
|
||||
constraint: hysteresis > 0
|
||||
constraint: hysteresis < (maxTemp - minTemp) / 2
|
||||
constraint: calibrationOffset >= -10
|
||||
constraint: calibrationOffset <= 10
|
||||
|
||||
// Safety constraint - deviation must be within bounds
|
||||
constraint: implies(safe, deviation <= hysteresis)
|
||||
constraint: implies(not safe, deviation > hysteresis)
|
||||
|
||||
// Temperature range constraints
|
||||
constraint: currentTemp >= minTemp - 20 // Allow temporary excursions
|
||||
constraint: currentTemp <= maxTemp + 20
|
||||
constraint: ambientTemp >= -40
|
||||
constraint: ambientTemp <= 85
|
||||
|
||||
// Verification: alert logic is correct
|
||||
verify: always(implies(
|
||||
currentTemp > maxTemp + hysteresis,
|
||||
alert
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
currentTemp < minTemp - hysteresis,
|
||||
alert
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
alert,
|
||||
action in [EmergencyShutDown, Warning, Override]
|
||||
))
|
||||
|
||||
verify: always(implies(
|
||||
not alert,
|
||||
action == NormalOperation
|
||||
))
|
||||
|
||||
// Events for safety audit trail
|
||||
event TemperatureReading {
|
||||
sensorId: String
|
||||
temperature: Real
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event TemperatureAlert {
|
||||
sensorId: String
|
||||
temperature: Real
|
||||
threshold: Real
|
||||
alertType: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event SafetyAction {
|
||||
sensorId: String
|
||||
action: String
|
||||
timestamp: Nat
|
||||
}
|
||||
|
||||
event CalibrationWarning {
|
||||
sensorId: String
|
||||
offset: Real
|
||||
reason: String
|
||||
timestamp: Nat
|
||||
}
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue