Time-utility scheduling and provably correct critical computer-based systems

Summary form only given. We investigate ways of expanding the scope of applicability of time-utility and aggregate utility driven scheduling. Being interested in critical applications and systems, we explore issues raised with proving that a system is endowed with combined safety, liveness, timeliness and dependability properties, and the province of proof-based system engineering. We examine the nature of proof obligations, as well as how to fulfill them, whenever timeliness and aggregate utility properties are sought. Relationships with classical real-time computing problems and timeliness proofs are analyzed. Then we take time-utility scheduling a few steps further, by showing how to maximize aggregate utility while achieving process serializability, process termination, as well as dependability properties, in various computational models, considering distributed systems prone to failures where processes share multicopied updatable persistent data.