Soft Models for Analysing Real-Time properties (Robyn SMART) (20pt or 12pt)

Meet Robyn, our Evolution ER1 robot (ER1 Robot Page 2004). In this project you will extend compositional performance models to predict "soft real-time" properties of Robyn, and design experiments to validate these. This will involve extending an existing package written in Java (Schmidt et al. 2003) and becoming more experienced with Markov Chain analysis. Robyn and other real time systems have requirements on their ``extra-functional'' properties, such as resource (CPU and memory) requirements, performance over time, reliability, and quality of service. "Soft real-time" properties take into account probability, for instance "executes program in 12s with 0.6 probability assuming collision probability less than 0.1". As industry moves to component-based software engineering, predicting extra-functional properties compositionally remains a challenging research problem (Schmidt 2003) for realistically sized systems. The Evolution ER1 is a robotics kit with computer vision, hearing, speech, networking, remote control, email, autonomous mobility, gripping, and IR sensing capabilities, implemented under Windows(TM) and Linux, and controllable via simple state machines or even remotely via a character-based TCP/IP API. The ER1 is suitable for use in a wide range of concept demonstration and prototyping scenarios, which have real-time aspects.

In this project you will develop a new moderately-sized state machine model of recovery-oriented interactions between independent autonomous software components. Recovery oriented computing (Patterson 2000) branches into exceptional behaviour before a failure occurs, i.e., proactively, for instance triggered by panicking components. Immediate and efficient measures are taken to safeguard the computation and lower the failure probability - overall mean time to recovery shortens and availability increases. Contrast this with reactive fault-tolerance where exceptions are thrown and handled after a failure is detected. Think 'alert' instead of 'failure' or 'exercise' instead 'hospital bed'.
Your model demonstrator will be implemented by extending an existing Java package for probabilistic finite state automata (PFSAs) (Jayaputera 2003). PFSAs serve as abstract models of programs (particularly in real-time and distributed, i.e., networked, systems). These models can be checked against expected properties including failure probabilities. Such properties are expressed in probabilistic temporal logic (PRISM home page) and checked symbolically against your abstract PFSA model or against actual executions of deployed and running software which is claimed to be recovery-oriented as modeled in the PFSA. The symbolic (model checking) executions could also form the basis for automated testing. Automata-based model checking has numerous practical applications in industry in advanced telecommunication, military and technical domains such as automotive software engineering.
While there are many challenging open problems with this novel recovery-oriented approach (Fox & Patterson 2003, Shapiro 2004) the scope of this Honours project is limited to developing the one model, implementing and exploring it as a model-checking case study.