-
Erol Gelenbe : Power Aware ICT and Network Management
Abstract : ICT is responsible for 2% of CO2 emissions in the world and it is expected that despite efforts to improve energy efficiency in computer systems and networks, this figure will increase by some 4% per year to attain 1.43B Tons per year in 2020.This paper will describe methods based on performance management which may reduce this continuing increase. In particular, networks and telecommunications equipment are expected to account for 25% of the total, while data centres may account for 18%. Thus we will also discuss network management techniques that can trade-off quality of service against energy consumption.
-
Daniel Kroening : Proving Program Termination
Abstract : Software bugs related to liveness can be particularly annoying; the program "gets stuck", and the user is left wondering whether it will resume responding. Liveness-related bugs are therefore an important target for program analysis. Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of ranking relations to prove program termination. We provide an experimental evaluation over a broad set of Windows drivers, and demonstrate that our algorithm is often able to conclude termination by examining only a small fraction of the program.
As a consequence, our algorithm is able to outperform known approaches by multiple orders of magnitude. The talk will contain some tutorial content on the state-of-the art techniques; no prior knowledge of termination analysis is assumed.
-
Jean-Jacques LESAGE : Tailor-made vs. formal languages: how to reconcile effectiveness and rigour of modeling for automation engineering?
Abstract : Tailor-made languages are used by most engineers for carrying out the different steps of the design cycle of industrial automation systems. These languages have been designed specifically to answer engineering needs. They often combine power of expression, simplicity of reading and large fields of application. Furthermore, these languages are often standards and are required for certification. Nevertheless, formal analysis of so built models is not possible. For so designed systems, formal validation/verification of performances, of safety or dependability properties, is then difficult and can be carried out only by using techniques like simulation.
In the last decade, researchers have proposed two different philosophies for introducing formal approaches in the design cycle. The first approach is to propose to engineers to use “classical” formal languages/methods/tools for specifying, designing and/or implementing controllers. We show that most of these attempts have not been successful. The second approach aims at preserving the use of tailor-made languages by engineers. The idea is rather to give these languages a formal semantics that is “hidden to the user” and allows formal analysis by using specific interfaces. LURPA lab is one of the originators of this second approach and has a twelve years experience in formalization of tailor-made languages.
To support this opinion and to illustrate this talk, the case of two tailor-made languages for preliminary risks analysis is studied. Firstly, we show how an algebraic formalization of Dynamic Fault Trees (DFT) makes the qualitative and the quantitative analysis possible in a formal way. Afterwards, a formalization of Boolean Driven Markov Processes (BDMP) by language theory and finite automata is proposed. In both cases, the original semantics of the languages has been preserved, but a formal “hidden layer” makes the formal analysis of these two tailor-made languages possible.
