iSAQB CPSA-A FM

Description

Attending the iSAQB® CPSA-A Formal Methods (FM) course gives participants 20 Technical Competence (TC) and 10 Methodological Competence (MC) towards the 70 points required for eligibility for the iSAQB CPSA-A exam with Brightest. It is important to remember that as part of the 70 points required to take the iSAQB CPSA-A exam with Brightest, you will need at least ten competence points in each of the following areas: 

• Technical Competence (TC)
• Methodological Competence (MC)
• Communicative Competence (CC)

Accredited iSAQB® FM - Formal Methods (CPSA-A) training is based on the current iSAQB® curriculum:

Part 1 - Logic

• Know the basic structure of propositional logic
• Know the basic structure of predicate/first-order logic
• Know the basic structure of temporal operators
• Understand the basic concepts of a logical calculus
• Understand the difference between intuitionistic and classical logic

Part 2 -  Specification and Implementation

• Differentiate notions of specification
• Understand that specifications may pertain to different kinds of components
• Understand that specifications may pertain to different qualities
• Differentiate between formal specifications and other types of specifications
• Know the distinguishing properties of at least three different specification languages
• Understand the notion of refinement

Part 3 - Formal Methods and the Development Process

• Identify where formal methods are applicable
• Know relevant qualities that indicate the use of formal methods
• Understand the relevance of precise specification
• Know tradeoffs between formal methods
• Introduce formal methods gradually
• Select appropriate formal methods
• Evaluate architecture with formal methods

Part 4 - Tools

• Apply property-based testing
• Understand the role of type systems
• Apply model checking to verify properties of automata
• Apply proof assistants to verify properties of arbitrary software systems
• Apply SMT solvers to verify constraints of arbitrary software systems
• Apply abstract interpretation to predict dynamic behavior statically