Analyzing Functional and Non Functional Attributes of Software Artifacts
Lecturer:
Prof. Ali Mili (New Jersey Institute of Technology)
Prof.Ali Mili earned the Doctorat de Troisieme Cycle from the Joseph Fourier University of Grenoble (France), the PhD from the University of Illinois (USA), and the Doctorat es-Sciences d’Etat from the Joseph Fourier University of Grenoble (France). He is currently working at the New Jersey Institute of Technology, and is affiliated with the Graduate Faculty at Rutgers-Newark. His research interests are in software engineering, ranging from technical to managerial/ organizational aspects; he has published ten books, twelve book chapters, and more than 200 journal and conference papers on these topics. He has worked in Africa (Tunisia, Algeria), Europe (France, Austria), North America (USA, Canada), Asia (Saudi Arabia, China) and Australia (Queensland, South Australia).
Place:
National Institute of Informatics, 20fl. Lecture room 2001(Dec.20: Lecture room 2010)
Work done with R.K. Abercrombie (ORNL), Anis Ben Aissa (FST, Tunis), and F.T. Sheldon (ORNL).
Tuesday, December 13, 2011, 13:30-15:00, Lecture room 2001, 20fl.
We propose to measure system dependability by means of a new concept, the mean failure cost; in this talk, we focus on using this metric to represent security, then discuss how the same metric can be used to model reliability, safety, and availability. As a measure of security, the mean failure cost offers the following attributes:It is not intrinsic to the system, but is also dependent on the system stakeholders.
oIt is not an abstract number on an arbitrary scale, but represents a meaningful econometric function.
oIt reflects the heterogeneity of stakeholder communities: not all stakeholders are created equal (some have bigger stakes in the operation of the system than others).
oIt reflects the heterogeneity of security requirements: not all security requirements are created equal (violating some requirements may cause greater loss than violating others).
oIt reflects the heterogeneity of system architectures: not all components are created equal (some components may be more critical to system operation than others).
oIt reflects the heterogeneity of threat configurations: not all security threats are created equal (some may have greater impact on system components than other).
We discuss how this metric is defined, how it can be computed, and how it can be used for rational quantitative decision making pertaining to system security.
Work done with Kh. Bsaies (FST, Tunis), J. Desharnais (Laval, Quebec), W. Ghardallou (FST, Tunis), L. Labed Jilani (USG, Tunis), A. Louhichi (FST, Tunis), O. Mraihi (ISG, Tunis).
Tuesday, December 20, 2011, 13:30-15:00, Lecture room 2010, 20fl.
Despite the emergence of many programming languages and programming paradigms, most of the code being developed and maintained nowadays is written in C-like programming languages, perhaps with an OO twist. In such code, loops are an important locus of complexity, hence an important source of errors, and an important focus of program analysis. Since their introduction in 1969, invariant assertions have, justifiably, played an important role in the analysis and verification of while loops; in this talk, we introduce a new concept, viz invariant relations, and discuss its relation to invariant assertions and invariant functions.
Work done with Kh. Bsaies (FST, Tunis), J. Desharnais (Laval, Quebec), W. Ghardallou (FST, Tunis), L. Labed Jilani (USG, Tunis), A. Louhichi (FST, Tunis), O. Mraihi (ISG, Tunis).
Tuesday, December 27, 2011, 13:30-15:00, Lecture room 2001, 20fl.
In this talk we discuss the use of invariant relations in the analysis of while loops. Specifically, we show how we can use invariant relations to perform the following analysis on while loops:
oCompute inductive assertions,
oCompute invariant assertions,
oCompute or approximate loop functions,
oCompute weakest precondition of loops,
oCompute or approximate strongest postconditions of loops,
oCompute or approximate the (largest) space within which the loop is guaranteed to terminate.
Work done with L. Labed Jilani (ISG, Tunis) and I. Derbel (ISG, Tunis).
Tuesday, January 10, 2012, 13:30-15:00, Lecture room 2001, 20fl.
Ideally, we want to think of the software architecture phase of a product lifecycle as the phase when the non functional attributes of the product are determined; a disciplined approach to software architecture consists in identifying the non functional attributes that we want to optimize for the product at hand, and architecting the system accordingly, perhaps at the expense of other desirable attributes. Yet, many current architectural description languages offer no means to represent non functional attributes of architectural components, and (to the best of our language) none offer any means to (automatically) reason about them. In this talk, we discuss our work in defining an architectural description language as an extension of ACME, and in designing a compiler for this language that enables us to compute system-wide attributes from component-level attributes. The talk concludes with a demo of the tool on a sample example.
Friday, January 13, 2012, 13:30-15:00, Lecture room 2001, 20fl.
This research emerged from two teaching concerns, and has evolved to become a topic of applied/ applicable research. The original teaching concerns were:
oHow to teach a data structures course at the undergraduate level in a way that promotes the disciplines of modular design/ bottom up programming/ information hiding?
oHow to teach formal methods of V&V at the graduate level while making the material accessible?
The result is a discipline for the specification, validation, design and verification of software modules, that encompasses the following phases:
oRequirements Analysis,
oFormal Specification Generation,
oFormal Specification Validation,
oFormal Product Verification,
oProduct Testing,
oReliability Estimation.
The whole methodology is sufficiently lightweight that graduate students learn all its phases in a fifteen week semester and apply it on non-trivial examples.
