Architecture
This chapter discusses the architecture of PLCverif.
Platform and metamodels. PLCverif is a platform for (PLC) program analysis, mainly for formal verification, but also for testing and static analysis. It provides:
- A unified workflow model for program analysis (
Job
),- A verification-specific implementation of this workflow model is also included (
VerificationJob
). This defines the concept of verification requirements, verification backends, verification reports.
- A verification-specific implementation of this workflow model is also included (
- Common metamodels to describe analysis problems (Expression and CFA metamodels),
- Platform-level support for:
- Language frontend handling (which are responsible for parsing programs and representing them as CFAs),
- CFA reductions,
- Unified serialization and deserialization of job configuration (
Settings
).
Core library. Besides the platform definition, PLCverif contains a library of core functionalities. This includes built-in jobs (verification job), and verification backends, CFA reductions and verification reporters for the verification job. The core libraries are discussed in the next chapter.