Abstract
Recent years have seen the arrival of the Internet as the platform that supports most areas within organizations, a fact which has led to the appearance of specific methodologies and tools for the construction of Web information systems (WIS). However, an absence of functionalities for the verification and validation (V&V) has been detected in the methodologies and tools of the models which have been built. This chapter presents one of these methodologies for WIS development (MIDAS) and shows how it has been completed with the definition of a strategy for the formal specification of its models with V&V objectives. This will contribute to increasing the quality of the models used in WIS development. The plug-in architecture which integrates this formal approach within CASE tools for WIS development is also shown.
Key Terms in this Chapter
Model-Driven Development: Its defining characteristic is that software development’s primary focus and products are models rather than computer programs. The main advantage of this is that we express models using concepts that are much less bound to the underlying implementation technology and are much closer to the problem domain relative to most popular programming languages. This makes the models easier to specify, understand, and maintain; in some cases, it might even be possible for domain experts, rather than computing technology specialists, to produce systems. It also makes models less sensitive to the chosen computing technology and to evolutionary changes to that technology (the concept of platform-independent models is often closely connected to MDD).
Formal Specification: Description of a model in a comprehensive and consistent way; a model can be given, for example, for an application domain, for a requirement or a set of requirements, for a software architecture, or for a program organization. It is expressed in a formal language. A formal language specifies at meta-level a syntax, a semantics, and a proof system.
Validation: Validation analyzes whether the observable behaviour of a system is in agreement with the requirements. With regard to validation techniques, one of the most used is the scenarios and use-case simulation. This technique analyzes the system behaviour in order to ensure that it is the same as the functionality expected of the system. Simulation languages (as ASL) or tools (as Statemate) can be used.
Maude: Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude is an extensible and powerful language that allows many advanced metaprogramming and metalanguage applications. Some of the most interesting applications of Maude are metalanguage applications, in which Maude is used to create executable environments for different logics, theorem provers, languages, and models of computation.
Model / Metamodel: A model is a set of statements about some system under study. Here, statement means some expression about the SUS that can be considered true or false (although no truth value has necessarily to be assigned at any particular point in time). We can use a model to describe an SUS. In this case, we consider the model correct if all its statements are true for the SUS. A metamodel is a specification model for a class of SUS, where each SUS in the class is itself a valid model expressed in a certain modelling language. That is, a metamodel makes statements about what can be expressed in the valid models of a certain modelling language.
User-Services-Oriented: A way to address the construction of the navigation model of Web Information System; the method is based on identifying conceptual user services, that is, specific services required by the user. Like this, the navigation model is focused on identifying the services required by the user and one specific route for each one of those user services that guides the navigation of the user through the WIS.
Verification: Verification tries to show that a system is being built correctly. Usually, it involves satisfying specific properties of the diagram metamodels or properties related to the system domain. This verification can be made using formal or informal methods. Checklists and algorithms, which analyze a model looking for errors or abnormal situations, are informal verification techniques. Theorem proving and model checking are formal verification techniques.
Web Engineering: This is a relatively new branch of software engineering, which addresses the specific issues related to design and development of large-scale Web applications. In particular, it focuses on the methodologies, techniques, and tools that are the foundation of complex Web application development and which support their design, development, evolution, and evaluation.