Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.

Exploring design patterns for sustainable behaviour

Products and services explicitly intended to influence users’ behaviour are increasingly being proposed to reduce environmental impact and for other areas of social benefit. Designing such interventions often involves adopting and adapting principles from other contexts where behaviour change has been studied. The ‘design pattern’ form, used in software engineering and HCI, and originally developed in architecture, offers benefits for this transposition process. This article introduces the Design with Intent toolkit, an idea generation method using a design pattern form to help designers address sustainable behaviour problems. The article also reports on exploratory workshops in which participants used the toolkit to generate concepts for redesigning everyday products—kettles, curtains, printers and bathroom sinks/taps—to reduce the environmental impact of use. The concepts are discussed, along with observations of how the toolkit was used by participants, suggesting usability improvements to incorporate in future versions.

John Frazer

John Frazer, Professor, trained at the Architectural Association, taught first at Cambridge University and then the AA in the 1970s and again in the '90s. He was Head of School of Design Research History and Criticism at the University of Ulster in the 1980s, he also ran a systems and design consultancy with his wife Julia (including projects for Cedric Price and Walter Segal) and was founder and chairman of Autographics software. He is currently Swire Chair Professor and Head of School of Design in Hong Kong.----- This is a very personal perspective on a concept of universal and future significance. It is personal, both is the sense that it is an unashamedly biased view of both the significance of the project, and the nature of that significance and because the author was personally involved as one of the consultants on GENERATOR and subsequently involved Cedric Price in its educational application at the Architectural Association. GENERATOR is still very much alive and was still developing whilst this chapter was being written.

The generation of virtual prototypes for performance optimization

I am suspicious of tools without a purpose - tools that are not developed in response to a clearly defined problem. Of course tools without a purpose can still be useful. However the development of first generation CAD was seriously impeded because the solution came before the problem. We are in danger of repeating this mistake if we do not clarify the nature of the problem that we are trying to solve with the next generation of tools. Back in the 1980s I used to add a postscript slide at the end of CAD conference presentations and the applause would invariably turn to concern. The slide simple asked: can anyone remember what it was about design that needed aiding before we had computer aided design?

Tangible interfaces to explain Gaudi's use of ruled-surface geometries

This paper summarises the development of a machine-readable model series for explaining Gaudi's use of ruled surface geometry in the Sagrada Familia in Barcelona, Spain. The first part discusses the modeling methods underlying the columns of the cathedral and the techniques required to translate them into built structures. The second part discusses the design and development of a tangible machine-readable model to explain column-modeling methods interactively in educational contexts such as art exhibitions. It is designed to explain the principles underlying the column design by means of physical interaction without using mathematical terms or language.

Interactive architecture

This chapter explores the development of concepts of interactive environments by comparing two major projects that frame the period of this book. The Fun Palace of 1960 and the Generator of 1980 both proposed interactive environments responsive to the needs and behaviour of their users, but the contrast in terms of the available technology and what it enabled could not be more marked. The Fun Palace broke new architectural, organizational and social ground and was arguably the first proposition for cybernetic architecture; the Generator demonstrated how it could be achieved. Both projects are now acknowledged as seminal architectural propositions of the twentieth century, and both were designed by Cedric Price.

From concept to embodiment : challenge and strategy

Facing with the difficulty in information propagation and synthesizing from conceptual to embodiment design, this paper introduces a function-oriented, axiom based conceptual modeling scheme. Default logic reasoning is exploited for recognition and reconstitution of conceptual product geometric and topological information. The proposed product modeling system and reasoning approach testify a methodology of "structural variation design", which is verified in the implementation of a GPAL (Green Product All Life-cycle) CAD system. The GPAL system includes major enhancement modules of a mechanism layout sketching method based on fuzzy logic, a knowledge-based function-to-form mapping mechanism and conceptual form reconstitution paradigm based on default geometric reasoning. A mechanical hand design example shows a more than 20 times increase in design efficacy with these enhancement modules in the GPAL system on a general 3D CAD platform.

A natural model for architecture : the nature of the evolutionary model 1995

John Frazer's architectural work is inspired by living and generative processes. Both evolutionary and revolutionary, it explores informatin ecologies and the dynamics of the spaces between objects. Fuelled by an interest in the cybernetic work of Gordon Pask and Norbert Wiener, and the possibilities of the computer and the "new science" it has facilitated, Frazer and his team of collaborators have conducted a series of experiments that utilize genetic algorithms, cellular automata, emergent behaviour, complexity and feedback loops to create a truly dynamic architecture. Frazer studied at the Architectural Association (AA) in London from 1963 to 1969, and later became unit master of Diploma Unit 11 there. He was subsequently Director of Computer-Aided Design at the University of Ulter - a post he held while writing An Evolutionary Architecture in 1995 - and a lecturer at the University of Cambridge. In 1983 he co-founded Autographics Software Ltd, which pioneered microprocessor graphics. Frazer was awarded a person chair at the University of Ulster in 1984. In Frazer's hands, architecture becomes machine-readable, formally open-ended and responsive. His work as computer consultant to Cedric Price's Generator Project of 1976 (see P84)led to the development of a series of tools and processes; these have resulted in projects such as the Calbuild Kit (1985) and the Universal Constructor (1990). These subsequent computer-orientated architectural machines are makers of architectural form beyond the full control of the architect-programmer. Frazer makes much reference to the multi-celled relationships found in nature, and their ongoing morphosis in response to continually changing contextual criteria. He defines the elements that describe his evolutionary architectural model thus: "A genetic code script, rules for the development of the code, mapping of the code to a virtual model, the nature of the environment for the development of the model and, most importantly, the criteria for selection. In setting out these parameters for designing evolutionary architectures, Frazer goes beyond the usual notions of architectural beauty and aesthetics. Nevertheless his work is not without an aesthetic: some pieces are a frenzy of mad wire, while others have a modularity that is reminiscent of biological form. Algorithms form the basis of Frazer's designs. These algorithms determine a variety of formal results dependent on the nature of the information they are given. His work, therefore, is always dynamic, always evolving and always different. Designing with algorithms is also critical to other architects featured in this book, such as Marcos Novak (see p150). Frazer has made an unparalleled contribution to defining architectural possibilities for the twenty-first century, and remains an inspiration to architects seeking to create responsive environments. Architects were initially slow to pick up on the opportunities that the computer provides. These opportunities are both representational and spatial: computers can help architects draw buildings and, more importantly, they can help architects create varied spaces, both virtual and actual. Frazer's work was groundbreaking in this respect, and well before its time.

In the beginning...

Professor John Frazer and architect Gianni Botsford met as tutor and student in 1994 at the Architural Association. Two years of never talking about architecture and nearly burning the studio down led to a new way of approaching design.

H'ani : National Parks and Wildlife Facilities at Springbrook.

The paper describes the process in whcih a multi-disciplinary group of design students propose a redevelopment of individual and group camping facilities at Springbrook national Park. A romantic and fairyland atmosphere is developed to enhance the natural educational potential of the site and heighten the experience of the transient community, the campers.

Space and culture: Tradition verses culture

This paper proposes to examine contemporary culture, through communication and technology, in an attempt to expose some of these new or altered spatial concepts evident in film and built form, such as ratefaction and saturation

Existential experience : the unfolding

This paper reports on a project concerned with the relationship between person and space in the context of achieving a contemplative state. The need for such a study originated with the desire to contribute to the design of multicultural spaces which could be used for a range of activities including prayer and meditation. Given that the words ‘prayer’ and ‘meditation’ are highly value-laden and potentially alienating for some people, it was decided to use the more accessible term ‘contemplative’. While the project is still underway,several findings have emerged that can be reported on and are of relevance to the conference both methodologically and substantively. Informed by phenomenological methodology, data were collected from a diverse group of people using photo-elicitation and interviewing. The technique of photo-elicitation proved to be highly effective in helping people to reveal their everyday lived experience of contemplative spaces. This methodological aspect of the project is described more fully in the paper. The initial stage of analysis produced two categories of data: varying conceptions of contemplation and contemplative space; and, common understandings of contemplation and contemplative space. From this it was found that achieving a state of contemplation involves both the person and the environment in a dialectic process of unfolding. The unfolding has various physical, psycho-social, and existential dimensions or qualities which operate sequentially and simultaneously. In the paper, these are labelled:the unfolding of the core; distinction; manifestation; cleansing; creation; and sharing, and have parallels with Mircea Eliade’s 1959 definition of sacred as 'something that manifests itself, shows itself, as something wholly different from the profane’. It also connects with the views of Nishida Kitaro from the Kyoto School of Philosophy on the theme of ‘absolute nothingness’: ‘the body-mind is dropped off and we are united with the consciousness of absolute nothingness’ (Kitaro in Heisig, 2001, p. 169). According to Marion (2005), ‘nothingness’ is defined by givenness. In the paper, this fold of givenness is interpreted in the context of the qualities of the environment that accomplish the act of coming forward into visibility through the dialectic relationship with a person. (Eliade, 1959, Heisig, 2001, Marion, 2002)

Experimental methodology report

In architectural design and the construction industry, there is insufficient evidence about the way designers collaborate in their normal working environments using both traditional and digital media. It is this gap in empirical evidence that the CRC project, “Team Collaboration in High Bandwidth Virtual Environments” addresses. The project is primarily, but not exclusively, concerned with the conceptual stages of design carried out by professional designers working in different offices. The aim is to increase opportunities for communication and interaction between people in geographically distant locations in order to improve the quality of collaboration. In order to understand the practical implications of introducing new digital tools on working practices, research into how designers work collaboratively using both traditional and digital media is being undertaken. This will involve a series of empirical studies in the work places of the industry partners in the project. The studies of collaboration processes will provide empirical results that will lead to more effective use of virtual environments in design and construction processes. The report describes the research approach, the industry study, the methods for data collection and analysis and the foundation research methodologies. A distinctive aspect is that the research has been devised to enable field studies to be undertaken in a live industrial environment where the participant designers carry out real projects alongside their colleagues and in familiar locations. There are two basic research objectives: one is to obtain evidence about design practice that will inform the architecture and construction industries about the impact and potential benefit of using digital collaboration technologies; the second is to add to long term research knowledge of human cognitive and behavioural processes based on real world data. In order to achieve this, the research methods must be able to acquire a rich and heterogeneous set of data from design activities as they are carried out in the normal working environment. This places different demands upon the data collection and analysis methods to those of laboratory studies where controlled conditions are required. In order to address this, the research approach that has been adopted is ethnographic in nature and case study-based. The plan is to carry out a series of indepth studies in order to provide baseline results for future research across a wider community of user groups. An important objective has been to develop a methodology that will produce valid, significant and transferable results. The research will contribute to knowledge about how architectural design and the construction industry may benefit from the introduction of leading edge collaboration technologies. The outcomes will provide a sound foundation for the production of guidelines for the assessment of high bandwidth tools and their future deployment. The knowledge will form the basis for the specification of future collaboration products and collaboration processes. This project directly addresses the industry-identified focus on cultural change, image, e-project management, and innovative methods.

Living walls - a way to green the built environment

Actions Towards Sustainable Outcomes Environmental Issues/Principal Impacts The increasing urbanisation of cities brings with it several detrimental consequences, such as: • Significant energy use for heating and cooling many more buildings has led to urban heat islands and increased greenhouse gas emissions. • Increased amount of hard surfaces, which not only contributes to higher temperatures in cities, but also to increased stormwater runoff. • Degraded air quality and noise. • Health and general well-being of people is frequently compromised, by inadequate indoor air quality. • Reduced urban biodiversity. Basic Strategies In many design situations, boundaries and constraints limit the application of cutting EDGe actions. In these circumstances, designers should at least consider the following: • Living walls are an emerging technology, and many Australian examples function more as internal feature walls. However,as understanding of the benefits and construction of living walls develops this technology could be part of an exterior facade that enhances a building’s thermal performance. • Living walls should be designed to function with an irrigation system using non-potable water. Cutting EDGe Strategies • Living walls can be part of a design strategy that effectively improves the thermal performance of a building, thereby contributing to lower energy use and greenhouse gas emissions. • Including living walls in the initial stages of design would provide greater flexibility to the design, especially of the facade, structural supports, mechanical ventilation and watering systems, thus lowering costs. • Designing a building with an early understanding of living walls can greatly reduce maintenance costs. • Including plant species and planting media that would be able to remove air impurities could contribute to improved indoor air quality, workplace productivity and well-being. Synergies and References • Living walls are a key research topic at the Centre for Subtropical Design, Queensland University of Technology: http://www.subtropicaldesign.bee.qut.edu.au • BEDP Environment Design Guide: DES 53: Roof and Facade Gardens • BEDP Environment Design Guide: GEN 4: Positive Development – Designing for Net Positive Impacts (see green scaffolding and green space frame walls). • Green Roofs Australia: www.greenroofs.wordpress.com • Green Roofs for Healthy Cities USA: www.greenroofs.org