iSAQB CPSA-A FM

Descriere

Attending the iSAQB® CPSA-A Formal Methods (FM) course gives participants 10 Technical Competence (TC), 10 Methodological Competence (MC), and 10 Communicative Competence (CC) Points 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