Alan M. Davis · 1982
This paper describes a software tool, called the Feature Simulator, that "executes" formally written requirements specifications for real-time systems and enables users to "interact" with the simulated product at the completion of the requirements specification phase of the software life-cycle. This tool thus produces an early and rapid prototype with which customers, designers, and managers can verify that the product meets their needs and expectations. Any deficiencies that they find can then be corrected by inexpensive changes to the product's requirements specification, rather than by more costly modifications to the final product.
Cited by 4
Mirjana Ivanović, Viktor Kunčak · 2008
We propose a framework for specification of programming language semantics, abstract and concrete syntax, and lexical structure. The framework is based on Modular Monadic Semantics and allows independent specification of various language features. Features such as arithmetics, conditionals, exceptions, state and nondeterminism can be freely combined into working interpreters, facilitating experiments in language design. A prototype implementation of this system in Haskell is described and possibilities for more sophisticated interpreter generator are outlined. 1
Cited by 0
Hee, KM Kees van, Houben, GJPM Geert-Jan, Somers, LJAM Lou et al. · TU/e Research Portal (Eindhoven University of Technology) · 1988
Cited by 0
Hee, van, K.M., Somers, L.J.A.M., Voorhoeve, M. et al. · TU/e Research Portal · 1989
Cited by 0
Yves Leduc, Nathalie Messina · 2011
Cited by 0
Dieser Bericht Ist, Thomas Gehrke, Thomas Gehrke et al. · 1996
We present a new programming language ProFun which is aimed for the specification and prototype implementation of reactive systems. ProFun combines the paradigms of concurrent and functional programming. A formal operational semantics is developed as a basis for verification techniques. We have implemented a ProFun-compiler which uses C++ as its target language. Keywords: Executable Specifications, Language Design, Integration of Concurrent and Functional Programming, Formal Reasoning. 1 Introduction Reactive and distributed systems are of increasing importance in theory and practice of computer science. Various languages for the specification and implementation of reactive systems have been developed to integrate two major aspects of reactive systems: The description of the structure and dynamic behaviour of a system and the handling of data. Process algebras [Mil89, Hoa85] are commonly used to specify the reactions of a system on external events from its environment by mea...
Cited by 0
M. Sveda, Radimı́r Vrba · Computer · 2001
Combining hardware components with an executable specification language facilitates the specification prototyping of embedded distributed systems. The specification language should cover process management, timing, and communication commands that real-time executive and communication task services of every node prototype can interpret. We use a technique that employs attribute grammars and either a macro processor or Prolog to execute the language.
Cited by 20
Rolf Schwitter, Norbert E. Fuchs · ArXiv.org · 1996
Deriving formal specifications from informal requirements is difficult since one has to take into account the disparate conceptual worlds of the application domain and of software development. To bridge the conceptual gap we propose controlled natural language as a textual view on formal specifications in logic. The specification language Attempto Controlled English (ACE) is a subset of natural language that can be accurately and efficiently processed by a computer, but is expressive enough to allow natural usage. The Attempto system translates specifications in ACE into discourse representation structures and into Prolog. The resulting knowledge base can be queried in ACE for verification, and it can be executed for simulation, prototyping and validation of the specification.
Cited by 26Open access
Rummelhoff, Ivar, Kristoffersen, Thor, Østvold, Bjarte M. · Zenodo (CERN European Organization for Nuclear Research) · 2024
We propose a preservation method for relational databases and a corresponding tool. The method involves writing specifications that can later be executed without user interaction. This provides provenance and reproducibility, and it facilitates automation and an iterative preservation process.
Cited by 0Open access
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen et al. · Lecture notes in computer science · 2013
Cited by 6
Tuzhilin, Alexander, Balasubramanian, P., Ecole Nationale Superieure des Telecommunications, 75 - Paris (France). Dept. Informatique · OpenGrey (Institut de l'Information Scientifique et Technique) · 1994
Available at INIST (FR), Document Supply Service, under shelf-number : RP 12468 / INIST-CNRS - Institut de l'Information Scientifique et Technique
Cited by 0
Michela degli Innocenti, Giuliano Pacini, TURINI, FRANCO et al. · CINECA IRIS Institutial research information system (University of Pisa) · 1990
Cited by 0
M. Degl'Innocenti, Gian-Luigi Ferrari, G. Pacini et al. · IEEE Transactions on Software Engineering · 1990
RSF is a formalism for specifying and prototyping systems with time constraints. Specifications are given via a set of transition rules. The application of a transition rule is dependent upon certain events. The occurrence times of the events and the data associated with them must satisfy given properties. As a consequence of the application of a rule, some events are generated and others are scheduled to occur in the future, after given intervals of time. Specifications can be queried, and the computation of answers to queries provides a generalized form of rapid prototyping. Executability is obtained by mapping the RSF rules into logic programming. The rationale, a definition of the formalism, the execution techniques which support the general notion of rapid prototyping and a few examples of its use are presented.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
Cited by 19
K. Khordoc, M. Dufresne, E. Cerny et al. · Elsevier eBooks · 1993
Cited by 24
Ying Guan, Aditya Ghose · IEEE/WIC/ACM International Conference on Intelligent Agent Technology · 2006
Agent-oriented conceptual modelling (AoCM) notations such as i* have received considerable recent attention as a useful approach to early-phase requirements engineering. AoCM notations are useful in modeling organizational context and in offering high-level anthropomorphic abstractions as modeling constructs. AoCM notations such as i* help answer questions such as what goals exist, how key actors depend on each other and what alternatives must be considered. In this paper, we suggest an approach to executing i* models by translating these into set of interacting agents implemented in the 3APL language. In addition, we suggest a hybrid modeling, or co-evolution, approach in which i* models and 3APL agent programs are concurrently maintained and updated, while retaining some modicum of loose consistency between the two. This allows us to benefit from the complementary representational capabilities of the two frameworks.
Cited by 9
Simon Thompson · 1989
In this paper we give an example of the use of functional programming language in the specification and development of a program to solve a non-trivial problem.In particular, we show how we can give a direct implementation of a constructive specification (an execuiable specification, in other words) and then show how program transformation can be used to turn this specification into an efficient version of the program, using techniques from a standard library of transformations.We introduce the paper with a short review of functional programming.
Cited by 9Open access
Raz Yerushalmi · 2023
Deep reinforcement learning (DRL) has become a dominant paradigm for using deep learning to carry out tasks where complex policies are learned for reactive systems. However, these policies are “black-boxes”, e.g., opaque to humans and known to be susceptible to bugs. For example, it is hard - if not impossible - to guarantee that the trained DRL agent adheres to specific safety and fairness properties that may be required. This doctoral dissertation's first and primary contribution is a novel approach to developing DRL agents, which will improve the DRL training process by pushing the learned policy toward high performance on its main task and compliance with such safety and fairness properties, guaranteeing a high probability of compliance while not compromising the performance of the resulting agent. The approach is realized by incorporating domain-specific knowledge captured as key properties defined by domain experts directly into the DRL optimization process while leveraging behavioral languages that are natural to the domain experts. We have validated the proposed approach by extending the AI-Gym Python framework [1] for training DRL agents and integrating it with the BP-Py framework [2] for specifying scenario-based models [3] in a way that allows scenario objects to affect the training process through reward and cost functions, demonstrating dramatic improvement in the safety and performance of the agent. In addition, we have validated the resulting DRL agents using the Marabou verifier [4], confirming that the resulting agents indeed comply (in full) with the required safety and fairness properties. We have applied the approach, training DRL agents for use cases from network communication and robotic navigation domains, exhibiting strong results. A second contribution of this doctoral dissertation is to develop and leverage probabilistic verification methods for deep neural networks to overcome the current scalability limitations of neural network verification technology, limiting the applicability of verification to practical DRL agents. We carried out an initial validation of the concept in the domain of image classification, showing promising results.
Cited by 1
Kristoffer H. Rose · arXiv (Cornell University) · 2011
In this paper we outline how a simple compiler can be completely specified using higher order rewriting in all stages: parsing, analysis/optimization, and code emission, specifically using the crsx.sf.net system for a small declarative language called "X" inspired by XQuery (for which we are building a production quality compiler in the same way).
Cited by 1Open access
Kristoffer H. Rose · Electronic Proceedings in Theoretical Computer Science · 2011
In this paper we outline how a simple compiler can be completely specified using higher order rewriting in all stages: parsing, analysis/optimization, and code emission, specifically using the crsx.sf.net system for a small declarative language called "X" inspired by XQuery (for which we are building a production quality compiler in the same way).
Cited by 0Open access
Nils Fischer, Horst Salzwedel · SHILAP Revista de lepidopterología · 2012
Current avionics systems specifications, developed after conceptual design, have a high degree of uncertainty. Since specifications are not sufficiently validated in the early development process and no executable specification exists at aircraft level, system designers cannot evaluate the impact of their design decisions at aircraft or aircraft application level. At the end of the development process of complex systems, e. g. aircraft, an average of about 65 per cent of all specifications have to be changed because they are incorrect, incomplete or too vaguely described. In this paper, a model-based design methodology together with a virtual test environment is described that makes complex high level system specifications executable and testable during the very early levels of system design. An aircraft communication system and its system context is developed to demonstrate the proposed early validation methodology. Executable specifications for early conceptual system architectures enable system designers to couple functions, architecture elements, resources and performance parameters, often called non-functional parameters. An integrated executable specification at Early Conceptual Architecture Level is developed and used to determine the impact of different system architecture decisions on system behavior and overall performance.
Cited by 5Open access