iSAQB® FM
iSAQB CPSA-Advanced Level FM (Formal Methods) introduces formal methods that supplement traditional software architecture practices by using mathematical techniques to specify and verify critical system properties. Participants cover core topics such as logic , the link between specification and implementation , and how formal methods fit into the development process , supported by tools and practical examples.
Description
iSAQB CPSA-Advanced Level FM (Formal Methods) introduces formal methods that supplement traditional software architecture practices by using mathematical techniques to specify and verify critical system properties.
Participants cover core topics such as logic, the link between specification and implementation, and how formal methods fit into the development process, supported by tools and practical examples. The course focuses on how to design architectures that are amenable to formal verification, including the implications for language and tooling choices when connecting specification and code.
No sessions available
Check back later or contact a provider directly.
What You Will Learn
Module 1: Logic Fundamentals
Syntax and semantics of propositional and predicate (first-order) logic.
Temporal operators used to express time-dependent system properties.
Logical calculi and inference rules, including completeness and refutation.
Proof systems such as natural deduction, sequent calculus, and resolution.
Distinctions between classical and intuitionistic logic.
Module 2: Specification and Refinement
Formal specifications for functions, data types, algorithms, and system components.
Defining non-functional requirements including performance, security, and safety.
Comparison of specification languages such as Isabelle/HOL, ACL2, TLA+, and Alloy.
Refinement techniques and the use of intermediate models between specification and code.
Module 3: Formal Methods in the Development Lifecycle
Selection criteria for formal methods based on technical context and organizational needs.
Trade-offs between manual effort, expressiveness, and tool automation.
Strategies for the gradual introduction of formal methods into existing processes.
Using SMT/SAT solving and abstract interpretation to support architecture evaluation.
Module 4: Verification Tools and Techniques
Property-based testing to verify requirements with generated data.
Type systems and advanced typing concepts for static constraint checking.
Model checking to verify automata using temporal logic.
Proof assistants for deriving and verifying software system properties.
SMT solvers for checking constraints and mathematical proofs.
Abstract interpretation for predicting dynamic behavior, including pointer aliasing and data flow.
Module 5: Applied Examples
Practical application of formal methods to a specific system verification task or software architecture.
Certification & Exam
The iSAQB CPSA Advanced Level module FM (Formal Methods) is an accredited training module within the Certified Professional for Software Architecture, Advanced Level (CPSA-A) program.
Completing an FM course does not award a standalone “FM certificate”. Instead, it provides 30 credit points that count toward eligibility for the CPSA-A certification exam: 10 in Technical, 10 in Methodical, and 10 in Communicative competence.
To apply for CPSA-A certification, candidates must hold CPSA Foundation Level (CPSA-F), meet the experience prerequisites, and collect at least 70 credit points across at least three competence areas. The CPSA-A certification exam is based on an assignment, followed by assessment and an oral exam conducted by iSAQB-appointed experts.
Official sources: iSAQB CPSA-A Module FM page, FM Curriculum (EN).
What You Will Achieve
Course outcomes
Apply propositional logic, first-order (predicate) logic, and temporal logic operators to express system properties as precise formulas.
Analyze proof styles and logical calculi, including natural deduction, sequent calculus, and resolution, and distinguish classical from intuitionistic logic when selecting a reasoning approach.
Create formal specifications for functions, data types, algorithms, or whole systems, and differentiate between informal, formal, and mechanized specifications.
Design a refinement approach that links specification, intermediate models, and implementation, including identifying when a separate model is needed between specification and code.
Evaluate where formal methods fit in the development process, including selecting suitable methods based on target qualities such as functionality, performance efficiency, security, or safety.
Implement verification activities using selected tool families, including property-based testing, model checking, proof assistants, SMT solvers, and abstract interpretation, and interpret the resulting evidence and limitations.
Analyze type systems, including the role of dependent types, and assess how typing supports formal reasoning and verification of program properties.
Evaluate a software architecture with formal methods, including using SMT or SAT solving for architectural constraint problems and supporting architecture evaluation and continuous refinement.
Training Providers
1 providerFAQs
Get Custom In-house Training
Post once, get competitive offers from multiple providers. Choose the one that fits your team.
Similar Trainings
iSAQB® Foundation Level Certification (CPSA-F)
The iSAQB Foundation Level (CPSA-F) training covers software architecture design and documentation for small and medium systems. It teaches architects and developers how to turn requirements into technical structures. Key topics include: Architect roles and definitions. Design patterns and principles. Documentation methods for decisions. Quality evaluation techniques. Practical exercises and theory prepare participants for the official CPSA-F exam.
iSAQB® ADOC - Architecture Documentation Certification
The iSAQB® Architecture Documentation (ADOC) training is an Advanced Level module within the Certified Professional for Software Architecture (CPSA-A) program. The course shows how to document software architectures in a clear and structured way so that developers, architects, and stakeholders can understand and use them in real projects. Participants learn how to create architecture documentation that supports communication, decision making, and long term system maintenance. The training uses well known methods such as arc42 , common diagram types, and clear documentation rules that are widely used in professional software architecture work. The course also explains how good documentation helps teams share knowledge, reduce misunderstandings, and keep systems maintainable as they grow. Through practical examples and exercises, participants learn how to describe architecture decisions, structure documentation, and present complex systems in a simple and consistent way.
iSAQB® AGILA - Agile Software Architecture Certification
The iSAQB® AGILA module is an Advanced Level training course within the Certified Professional for Software Architecture – Advanced Level (CPSA-A) program. The course focuses on how software architecture works in agile development environments. Participants learn how to design and evolve software systems in agile teams where architectural responsibility is shared . The training shows how architects and developers make architecture decisions during short development cycles while keeping systems stable and maintainable. The course also explains how to balance architecture, speed, and quality in agile projects. Topics include collaborative design practices, continuous architecture work, and practical approaches for identifying and managing technical debt during iterative development.
iSAQB® ARCEVAL - Architecture Evaluation Certification
The iSAQB ARCEVAL course teaches systematic methods to evaluate software architectures. This module of the Certified Professional for Software Architecture (CPSA) Advanced Level helps professionals verify if a system meets its quality requirements. ATAM: Identifying risks and design trade-offs. Quality Models: Using ISO/IEC 25010 to define software quality. Review Techniques: Performing audits using checklists and walkthroughs. Economic Evaluation: Analyzing the cost-benefit of technical decisions. This training is for software architects and senior developers who must justify technical choices. Participants learn to document results and provide clear recommendations. Completion provides credit points toward the iSAQB CPSA-A certificate.
iSAQB® CLOUDINFRA - Advanced Level Certification
The iSAQB® CLOUDINFRA Training will familiarize you with the underlying concepts and implementation methods of dynamic cloud-native architectures . How can you operate applications reliably with containers, which methods can be used to set up a target-oriented monitoring system, how can you create a demand-oriented alerting system?
iSAQB® DDD - Domain Driven Design Training
iSAQB® Domain Driven Design (DDD) is an advanced iSAQB module where you can learn to develop a language and use DDD models to connect different applications. Using the sample apps, you can learn the individual steps in DDD training in tecnovy. It is an application-oriented and high-quality software architecture.