For more than a decade, UNSW has been developing methods and software to verify whether hardware or software systems meet given specifications. It checks the logic of the system to make sure it is correct. Has the software programmer implemented what they intended?
MCK (Model Checking Knowledge) is a novel model checker that supports several different ways of defining knowledge given a description of a multi-agent system and the observations made by the agents.
Although model checking can be used in a variety of applications, it is especially valuable for verifying software and hardware security.
Features and Benefits
• Determine if system is making optimal use of information
• Supports a range of knowledge semantics and choices of temporal language
• First system to extend capability to agent knowledge
• Used to analyse multi-agent systems with respect to properties stated in formal logic of knowledge, time and probability
Hardware security verification
Decision support tool
UNSW is seeking a partner to work with the researchers on further developing this technology for additional applications.