Verifying Complex Software Systems: the Challenge

Virtually all software applications grow in size and complexity over time.For software used in spacecraft, software size can even be shown to grow exponentially with each new mission flown, matching the growth trends seen in many other industries. This rapid growth poses a serious challenge to our ability to verify the reliability of complex safety-critical software systems. Significant progress has been made in the development of strong tool-based formal verification techniques in the last few decades, but the bar keeps rising. I will describe how we are tackling this challenge, and where the main research challenges in reliable systems design currently are.

Gerard Holzmann received his Ph.D. from Delft University of Technology in 1979. From 1980 until 2003 he was a researcher in the Computing Science Research Center of Bell Laboratories, in Murray Hill, New Jersey. He then moved to NASA/JPL in California to start the new Laboratory for Reliable Software, where he is currently a senior research scientist. He has published four books and many technical articles on software verification methods, image processing techniques, and telecommunication history. Dr. Holzmann is a member of the U.S. National Academy of Engineering. url: http://spinroot.com/gerard

Software Engineering Approaches to the Challenges in Technology Education and System Development in the Software Ecosystem Environment

There exist several challenges in the current science, engineering, mathematics (STEM) graduate education. We are continuously inundated with great volumes of information from our portable communication devices, lap tops, television etc., continuously. We do multitasking to assimilate the information resulting developing short attention spans. Our current digital generation spends enormous amount of time on social networking, video entertainment and video games. Science and engineering subjects require long and deep attention spans to learn and to contribute. We discuss some of the successful methods that can help us to focus on the deep topics of engineering and technology. These include video narratives, entertainment and gaming. We consider the instructional methods developed by ancient Greeks (Aristotle, Socrates etc.), and the teaching of moral principles by means of parables and narratives by Buddha and Christ. We consider the successful interest and curiosity creating violin teaching methods of Suzuki. We study the talent discovering and skill enhancing instructional methods of Montessori. The social networking and interactive type of instruction was used by Escalante to overcome academic weaknesses. The tweet- and- repeat methods of the Khan Academy also provide useful ideas for improving our teaching process using ICT technology. We propose a comprehensive cocktail (mixture) of methods as the transformative means to upgrade of STEM higher education based on similar ideas proposed and successfully used by Norman Borlaug, the Nobel Prize-winning agricultural biologist in agricultural crop production. His methods eliminated the unfortunate annual food famines in Mexico, China, and India. We propose a comprehensive software supported methods using graphical animation, using virtualization, immersion and video gaming techniques to capture interest and enhance creative skills. It is well known that we use only a small fraction of the total visual and sensual bandwidth that our nervous system and brain can process at any instant. We can expand our educational communication bandwidth input by innovative interactive graphical and aural presentations of our academic material for maximum advantage to create both interest, learning and to develop creative skills.

We introduce the theme of 'Needs Engineering' into our technical educational curriculum. This topic emphasizes the importance of problem (needs) finding, problem discovery and problem anticipation. We associate a 'problem' with a specific need. Needs and necessities are mothers of invention and innovation and therefore the prime factors in creative thinking. We describe the classification of problem-solution pairs using the Remsfeld paradigm of knowns-unknowns and their importance in creative problem finding and solving. Our educational system emphasizes problem solving under a known and well understood framework of theory and knowledge. It does not lead to creative thinking beyond the 'box'. It has been said that 'main object of teaching is not just how to solve problems and give explanations, but to knock at the doors of the mind'. Problems and needs- finding approaches are indeed the mothers of creative innovation. We quote a well known ICT company CEO:

"Today it is the minds, not the megahertz or the gigabytes that are scarce. Use IT (information technology) to enhance them and use them to deliver sustainable and survivable products to support our developing world".

In the second part of the presentation, we shall concentrate on software ecosystems and the sustainability issues of software entities. We see a large proliferation of platforms, app's, operating systems, designs, patterns etc. The concept of software ecosystem tries to develop an environment which nurtures, supports and evolves sustainable software systems. As in the natural ecosystem sustainability implies survivability in the short term and evolution and growth in the long term under changing environments, such as operating systems, languages, platforms, services etc. We develop a simple model of growth and give some examples. The theory involves the three basic resources, namely, intellectual resource (I), manual resources (M), and physical (P) resources, essential for our living. Intellectual resources grow in accordance with the law of increasing returns (Arthur and Romer); the manual resources follow the Churchill's suggestion of using minimum manual effort, and the natural physical resources follow the law of diminishing returns. We show that the basic tenets of our growth theory are similar to theory of evolution of human development. It is not a perfect theory. We are still working on it. It is just an hypothesis and yet provides another abstract way to look at evolution and provides some valuable insights on the software engineering trends of the future.

Evolving Critical Systems

Increasingly software can be considered to be critical, due to the business or other functionality which it supports. Upgrades or changes to such software are expensive and risky, primarily because the software has not been designed and built for ease of change. Expertise, tools and methodologies which support the design and implementation of software systems that evolve without risk (of failure or loss of quality) are essential. We address a research agenda for building software that (a) is highly reliable and (b) retains this reliability as it evolves, either over time or at run-time. We propose Evolving Critical Systems as an area for research to tackle the challenge and outline a number of scenarios to highlight some of the important research questions that should be asked of the community. Given that software evolution can be seen as a compromise between cost and risk, the most pressing question to ask is which processes, techniques and tools are most cost-effective for evolving critical systems?

Mike Hinchey is scientific director of Lero-the Irish Software Engineering Research Centre and a professor of software engineering at the University of Limerick, Ireland. His research interests include selfmanaging software and formal methods for system development. Hinchey received a PhD in computer science from the University of Cambridge. He is a senior member of the IEEE and currently chairs the IFIP Technical Assembly. url: [email protected]