System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation.
Hubert GaravelCésar VihoMassimo ZendriPublished in: Int. J. Softw. Tools Technol. Transf. (2001)
Keyphrases
- model checking
- formal specification
- formal methods
- formal verification
- process algebra
- temporal logic
- test generation
- model checker
- software testing
- temporal properties
- specification language
- concurrent systems
- computation tree logic
- finite state machines
- multiprocessor architecture
- symbolic model checking
- test cases
- bounded model checking
- epistemic logic
- quality assurance
- verification method
- multi agent
- information systems