No description available.

In order to remain competitive, modem systems developers are increasingly under pressure to produce software solutions to complex problems faster and cheaper, whilst at the same time maintaining a high level of quality in the delivered product. One of the key quality measures is the delivery of a system that meets the customer's requirements. Failure to meet the customer's requirements may engender significant re-design, which in turn will cost money, delay product introduction and may seriously damage the developer's credibility. For these reasons, the problem of developing a precise and unambiguous statement of requirements for a proposed system is perhaps one of the most challenging problems within software engineering today. Formal, model-based specification languages such as the Z notation have been widely adopted within the context of requirements engineering, to provide a vehicle for the development of precise and unambiguous specifications. However, the mathematical foundation upon which these notations are based often makes them unapproachable and difficult to assimilate by a non-specialist reader. The problem then faced is that if the customer cannot understand the semantics of the specification, how can the customer agree that the specification is indeed a true reflection of the requirements for the desired system? Several researchers have proposed that rapid prototyping and animation of specifications can be used to increase the customer's understanding of the formal specification. This is achieved by executing specification components on candidate data and observing that the behaviour is as expected. However this requires that the original formal specification be reliably transformed into a representation capable of being executed within a computer system. To achieve this aim requires the support of computer-based tools able to assist the requirements engineer in capturing, manipulating and transforming the formal specification in an efficient and consistent manner. This thesis describes the research and development of the TranZit tool, which is a Z notation editor, checker and transformation system. TranZit supports the efficient capture and maintenance of Z notation specifications using the Windows Graphical User Interface, supported by a suite of powerful language-driven features. In addition TranZit contains a highly integrated and optimised syntax and type checker, combining traditional compiler design techniques with innovative use of object-oriented data structures and methods, to assist the requirements engineer in ensuring the internal consistency of the captured specification. Most importantly, TranZit contains a novel transformation engine, which is capable of transforming a captured Z specification into an executable representation based on extensions to LISP, suitable for direct execution in an animation environment. This process is supported by an eclectic strategy combining automated transformation with user assistance, to overcome many of the well-documented problems associated with transforming non-executable clauses in formal specifications.

SystemC has emerged as a de facto standard modeling language for hardware and embedded systems. However, the current standard does not provide support for temporal specifications. Specifically, SystemC lacks a mechanism for sampling the state of the model at different types of temporal resolutions, for observing the internal state of modules, and for integrating monitors efficiently into the model's execution. This work presents a novel framework for specifying and efficiently monitoring temporal assertions of SystemC models that removes these restrictions. This work introduces new specification language primitives that (1) expose the inner state of the SystemC kernel in a principled way, (2) allow for very fine control over the temporal resolution, and (3) allow sampling at arbitrary locations in the user code. An efficient modular monitoring framework presented here allows the integration of monitors into the execution of the model, while at the same time incurring low overhead and allowing for easy adoption. Instrumentation of the user code is automated using Aspect-Oriented Programming techniques, thereby allowing the integration of user-code-level sample points into the monitoring framework. While most related approaches optimize the size of the monitors, this work focuses on minimizing the runtime overhead of the monitors. Different encoding configurations are identified and evaluated empirically using monitors synthesized from a large benchmark of random and pattern temporal specifications. The framework and approaches described in this dissertation allow the adoption of assertion-based verification for SystemC models written using various levels of abstraction, from system level to register-transfer level. An advantage of this work is that many existing specification languages call be adopted to use the specification primitives described here, and the framework can easily be integrated into existing implementations of SystemC.

Complex software-security policies are dicult to specify, understand, and update. The same is true for complex software in general, but while many tools and techniques exist for decomposing complex general software into simpler reusable modules (packages, classes, functions, aspects, etc.), few tools exist for decomposing complex security policies into simpler reusable modules. The tools that do exist for modularizing policies either encapsulate entire policies as atomic modules that cannot be decomposed or allow ne-grained policy modularization but require expertise to use correctly. This dissertation presents a policy-composition tool called PoliSeer [27, 26] and the PoCo policy-composition software-security language. PoliSeer is a GUI-based tool designed to enable users who are not expert policy engineers to exibly specify, visualize, modify, and enforce complex runtime policies on untrusted software. PoliSeer users rely on expert policy engineers to specify universally composable policy modules; PoliSeer users then build complex policies by composing those expert-written modules. This dissertation describes the design and implementation of PoliSeer and a case study in which we have used PoliSeer to specify and enforce a policy on PoliSeer itself. PoCo is a language for specifying composable software-security policies. PoCo users specify software-security policies in terms of abstract input-output event sequences. The policy outputs are expressive, capable of describing all desired, irrelevant, and prohibited events at once. These descriptive outputs compose well: operations for combining them satisfy a large number of algebraic properties, which allows policy hierarchies to be designed more simply and naturally. We demonstrate PoCo's capability via a case study in which a sophisticated policy is implemented in PoCo.

No description available.

Code modularization provides benefits throughout the software life cycle; however, the presence of crosscutting concerns (CCCs) in software hinders its complete modularization. Traditional modularization techniques work well under the assumption that code being modularized is functionally orthogonal to the rest of the code; as a result, software engineers try to separate code segments that are orthogonal in their functionality into distinct modules. However, in practice, software does not decompose neatly into modules with distinct, orthogonal functionality. In this thesis, we investigate the modularization of CCCs in software using two different techniques. Firstly, we discuss IVCon, a GUI-based tool that provides a novel approach to the modularization of CCCs. We have designed IVCon to capture the multi-concern nature of code. IVCon enables users to create, examine, and modify their code in two different views, the woven view and the unwoven view. The woven view displays program code in colors that indicate which CCCs various code segments implement, while the unwoven view displays code in two panels, one showing the core of the program and the other showing all the code implementing each concern in an isolated module. IVCon aims to provide an easy-to-use interface for conveniently creating, examining, and modifying code in, and translating between, the woven and unwoven views. Secondly, we discuss LoPSiL, which is a location-based policy-specification language. LoPSiL is Turing-complete and provides users with language constructs that enable them to manipulate location information; hence, LoPSiL can be used to specify and enforce generic policies that might involve location-based constraints. We have implemented a LoPSiL compiler using AspectJ, and we observe and discuss how the use of traditional units of modularization---aspects in this case---help modularize functionally orthogonal CCCs such as security and auditing.

Process patterns allow the modular modelling and adaptable application of business processes. Present descriptions of process patterns show defects like non-uniform and unequivocal description forms and missing relationship definitions. These defects disadvantageously affect the effective usage of process patterns. In this work we introduce the language PROPEL (Process Pattern Description Language), which provides concepts for the semiformal description of process patterns and relationships between process patterns. With the help of PROPEL single process patterns can be modelled and, by definition of relationships, be composed to more complicated processes. With the representation of different views of a process pattern catalog the process patterns and their relationships can be shown clearly. An example illustrates how a process pattern catalog and the contained process patterns are modelled. It is shown that in applying PROPEL the complexity of a process model can be reduced and inconsistencies of processes be eliminated.

The Object-Oriented Data Specification Framework (OODSF) is a C++ framework to facilitate programming in a heterogeneous distributed environment. Using the OODSF, C++ language bindings of commonly used specification languages, such as Abstract Syntax Notation 1 (ASN.l) and Interface Definition Language (IDL), can be defined. The OODSF defines C++ class libraries for ASN.l and IDL to simplify the C++ language bindings. Arbitrary application-level IDL and ASN.l specifications can be translated into C++ representations based on these class libraries. The OODSF contains facilities for encoding and decoding transferred data, allowing interoperability in a heterogeneous distributed system. A general interface is provided to encoding and decoding services so that a flexible choice of an encoding rule can be made. The current implementation of the OODSF contains external Encoding Rule (XDR) and Basic Encoding Rule (BER). / Master of Science

The increasing complexity of software systems has led to the development of sophisticated formal Methodologies for verifying and correcting data and programs. In general, establishing whether a program behaves correctly w.r.t. the original programmer s intention or checking the consistency and the correctness of a large set of data are not trivial tasks as witnessed by many case studies which occur in the literature. In this dissertation, we face two challenging problems of verification and correction. Specifically, verification and correction of declarative programs, and the verification and correction of Web sites (i.e. large collections of semistructured data). Firstly, we propose a general correction scheme for automatically correcting declarative, rule-based programs which exploits a combination of bottom-up as well as topdown inductive learning techniques. Our hybrid hodology is able to infer program corrections that are hard, or even impossible, to obtain with a simpler,automatic top-down or bottom-up learner. Moreover, the scheme will be also particularized to some well-known declarative programming paradigm: that is, the functional logic and the functional programming paradigm. Secondly, we formalize a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. We provide a rule-based, formal specification language which allows us to define syntactic as well as semantic properties of the Web site. Then, we formalize a verification technique which detects both incorrect/forbidden patterns as well as lack of information, that is, incomplete/missing Web pages. Useful information is gathered during the verification process which can be used to repair the Web site. So, after a verification phase, one can also infer semi-automatically some possible corrections in order to fix theWeb site. The methodology is based on a novel rewrit / Ballis, D. (2005). Rule-Based Software Verification and Correction [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1948

This thesis investigates the expressiveness of specification languages for stochastic safety-critical systems, addressing the need for expressiveness in describing system behaviour formally. Through a case study and specification language enhancements, the research explores the impact of different frameworks on a set of specifications. The results highlight the importance of continuous development in the specification languages to meet the complex behaviours of systems with probabilistic properties. The findings emphasise the need for extending the chosen specification languages more formally, to ensure that the languages can capture the complexity of the systems they describe.  The research contributes valuable insights into improving the expressiveness of specification languages for ensuring system safety and operational reliability.