Conventional genetic programming research excludes memory and iteration. We have begun an extensive analysis of the space through which GP or other unconventional AI approaches search and extend it to consider explici...
详细信息
ISBN:
(纸本)3540385932
Conventional genetic programming research excludes memory and iteration. We have begun an extensive analysis of the space through which GP or other unconventional AI approaches search and extend it to consider explicit program stop instructions (T8) and any time models (T7). We report halting probability, run time and functionality (including entropy of binary functions) of both halting and anytime programs. Turing complete program fitness landscapes, even with halt, scale poorly.
Object-Oriented Methods, Formal Specification Languages, Component-Based Software Production... This is just a very short list of technologies proposed to solve a very old and, at the same time, very well-known proble...
详细信息
ISBN:
(纸本)3540378715
Object-Oriented Methods, Formal Specification Languages, Component-Based Software Production... This is just a very short list of technologies proposed to solve a very old and, at the same time, very well-known problem: how to produce software of quality. programming has been the key task during the last 40 years, and the results have not been successful yet. This work will explore the need of facing a sound software production process from a different perspective: the non-programming perspective, where by non-programming we mainly mean modeling. Instead of talking about Extreme programming, we will introduce a Extreme Non-programming (Extreme Modeling-Oriented) approach. We will base our ideas on the intensive work done during the last years, oriented to the objective of generating code from a higher-level system specification, normally represented as a Conceptual Schema. Nowadays, though, the hip around MDA has given a new push to these strategies. New methods propose sound model transformations which cover all the different steps of a sound software production process from an Information systems Engineering point of view. This must include Organizational Modeling, Requirements Engineering, Conceptual Modeling and Model-Based Code Generation techniques. In this context, it seems that the time of Model Transformation Technologies is finally here...
Atomicity is an important generic specification that assures that a programmer can pretend blocks occur sequentially in any execution. We define a notion of atomicity based on causality. We model the control flow of a...
详细信息
ISBN:
(纸本)354037406X
Atomicity is an important generic specification that assures that a programmer can pretend blocks occur sequentially in any execution. We define a notion of atomicity based on causality. We model the control flow of a program with threads using a Petri net that naturally abstracts data, and faithfully captures the independence and interaction between threads. The causality between events in the partially ordered executions of the Petri net is used to define the notion of causal atomicity. We show that causal atomicity is a robust notion that many correct programs adopt, and show how we can effectively check causal atomicity using Petri net tools based on unfoldings, which exploit the concurrency in the net to yield automatic partial-order reduction in the state-space.
Verification and validation are two of the most critical issues in the software engineering process. Numerous techniques ranging from formal proofs to testing methods have been used during the last years to verify the...
详细信息
ISBN:
(纸本)3540330569
Verification and validation are two of the most critical issues in the software engineering process. Numerous techniques ranging from formal proofs to testing methods have been used during the last years to verify the conformity of a program with its specification. Recently, constraint programming techniques have been used to generate test data. In this paper we investigate the capabilities of constraint programming techniques to verify the conformity of a program with its specification. We introduce here a new approach based on a transformation of both the program and its specification in a constraint system. To establish the conformity we demonstrate that the union of the constraint system derived from the program and the negation of the constraint system derived from its specification is inconsistent (for the considered domains of values). This verification process consists of three steps. First, we generate a Boolean constraint system which captures the information provided by the control flow graph. Then, we use a SAT solver to solve the Boolean constraint system. Finally, for each Boolean solution we build a new constraint system over finite domains and solve it. The latter system captures the operational part of the program and the specification. Boolean constraints play an essential role since they drastically reduce the search space before the search and enumeration processes start. Moreover, in the case where the program is not conforming with its specification, Boolean constraints provide a powerful tool for finding wrong behaviours in different execution paths of the program. First experimental results on standard benchmarks are very promising.
We propose a model-based framework for developing a self-adaptive embedded program, which monitors its own execution and reconfigures itself at runtime to avoid failure and improve performance. Our approach uses forma...
详细信息
ISBN:
(纸本)0769527183
We propose a model-based framework for developing a self-adaptive embedded program, which monitors its own execution and reconfigures itself at runtime to avoid failure and improve performance. Our approach uses formal methods at different design stages to reduce the complexity of developing a self-adaptive embedded program. In our framework system requirement is rigidly encoded in temporal logics, and the original embedded system behavior is captured in a hybrid automaton-based model. We introduce the reconfiguration specification language REDL to specify reconfiguration requirements, and define a formal semantics of reconfiguration in context of hybrid automaton. Using formal methods also helps automate design and implementation: we use model-based runtime verification techniques introduced in [19] to extend a system model to a self-monitoring model based on its temporal logic requirements;we then extend the self-monitoring model with a reconfiguration mechanism based on its REDL specification. Our approach works with models, and hence it may be incorporated into existing model-based design workflow: the resulting self-adaptive model can be analyzed using an existing model simulator and may be used to generate a self-adaptive embedded program for targeted platform.
We seek for a small set of primitives that might serve as a basis for formalising and programming service oriented applications over global computers. As an outcome of this study we introduce here SCC, a process calcu...
详细信息
ISBN:
(纸本)3540388621
We seek for a small set of primitives that might serve as a basis for formalising and programming service oriented applications over global computers. As an outcome of this study we introduce here SCC, a process calculus that features explicit notions of service definition, service invocation and session handling. Our proposal has been influenced by Orc, a programming model for structured orchestration of services, but the SCC's session handling mechanism allows for the definition of structured interaction protocols, more complex than the basic request-response provided by Orc. We present syntax and operational semantics of SCC and a number of simple but nontrivial programming examples that demonstrate flexibility of the chosen set of primitives. A few encodings are also provided to relate our proposal with existing ones.
This paper focuses on the study of a new method for detecting masqueraders in computersystems. The main feature of such masqueraders is that they have knowledge about the behavior profile of legitimate users. The dat...
详细信息
ISBN:
(纸本)9783540490265
This paper focuses on the study of a new method for detecting masqueraders in computersystems. The main feature of such masqueraders is that they have knowledge about the behavior profile of legitimate users. The dataset provided by Schonlau et al. [1], called SEA, has been modified for including synthetic sessions created by masqueraders using the behavior profile of the users intended to impersonate. It is proposed an hybrid method for detection of masqueraders based on the compression of the users sessions and Hidden Markov Models. The performance of the proposed method is evaluated using ROC curves and compared against other known methods. As shown by our experimental results, the proposed detection mechanism is the best of the methods here considered.
In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchronously and concurrently on different threads. Th...
详细信息
ISBN:
(纸本)354037406X
In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchronously and concurrently on different threads. This paper investigates the problem of model checking programs that follow this idiom. We present a programming language SPL that encapsulates this design pattern. SPL extends simplified form of sequential Java to which we add the capability of making asynchronous method invocations in addition to the standard synchronous method calls and the ability to execute asynchronous methods in threads atomically and concurrently. Our main result shows that the control state reachability problem for finite SPL programs is decidable. Therefore, such multithreaded programs can be model checked using the counterexample guided abstraction-refinement framework.
In this paper we propose a dynamic code overlay technique of synchronous data-flow (SDF) -modeled program for low-end embedded systems which lack MMU-support. With this technique, the system can utilize expensive SRAM...
详细信息
ISBN:
(纸本)9783981080117
In this paper we propose a dynamic code overlay technique of synchronous data-flow (SDF) -modeled program for low-end embedded systems which lack MMU-support. With this technique, the system can utilize expensive SRAM memory more efficiently by using flash memory as code storage. SRAM is divided into several regions called overlay slots. A data-flow block or a cluster of data-flow blocks is loaded into the corresponding overlay slot on demand at run-time. Which blocks are clustered together and which overlay slots are allocated to the clusters are statically decided by the clustering and placement algorithm. We also propose an automatic code generation framework that generates the C-prograin code, dynamic loader and linker script files from the given SDF-modeled blocks and schematic, so we can run or simulate the program immediately without any additional coding effort. Experiments report that we can reduce the SRAM size significantly with a reasonable amount of time overhead for several real applications.
Program analysis techniques are used by software engineers to deduce and infer targeted characteristics of software systems for tasks such as testing, debugging, maintenance, and program comprehension. Recently, some ...
详细信息
ISBN:
(纸本)1595933751
Program analysis techniques are used by software engineers to deduce and infer targeted characteristics of software systems for tasks such as testing, debugging, maintenance, and program comprehension. Recently, some program analysis techniques have been designed to leverage characteristics of traditional experimentation in order to analyze software systems. We believe that the use of experimentation for program analysis constitutes a new program analysis paradigm: experimental program analysis. This research seeks to accomplish four goals: to precisely define experimental program analysis, to provide a means for classifying experimental program analysis techniques, to identify existing experimental program analysis techniques in the research literature, and to enhance the use of experimental program analysis by improving existing, and by creating new, experimental program analysis techniques.
暂无评论