Safe and Dependable Autonomous Systems - Formal Specification and Verification

This thesis will study the formal specification and verification of autonomous decision making of agents, accounting for safety constraints, in a context of non-deterministic actions and perception. This research may evolve towards bounded model checking or correct-by- construction policy generation. The results will be validated in a joint use case on the autonomous mobile robot.