检索结果-内蒙古大学图书馆

SOFTWARE ENGINEERING JOURNAL 1994年第4期9卷 174-182页

作者： GASKELL, C PHILLIPS, R UNIV HULL DEPT COMP SCIKINGSTON HULL HU6 7RXN HUMBERSIDEENGLAND

The idea of executing graphical system models is not new. Several accounts of research in this area are well documented. Despite this, such research is still in its infancy, particularly in relation to CASE environments and the practical application of ideas. The paper considers executability within CASE, with a focus on executable specifications. The importance of executability is highlighted, and some of the work in the field is noted. An experimental executable specification tool is presented. The final conclusions drawn take a look into the envisaged future of executability in CASE.

关键词： visual programming software tools formal specification executable specification tool Programming support Compilers, interpreters and other processors executable specifications Software engineering techniques program compilers CASE CASE environments executability graphical system models

来源：评论

学校读者我要写书评

暂无评论

executable specifications of resource-bounded agents

引用

AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS 2010年第3期21卷 368-396页

作者： Fisher, Michael Ghidini, Chiara Univ Liverpool Dept Comp Sci Liverpool L69 3BX Merseyside England FBK Irst Data & Knowledge Management Grp DKM I-38050 Trento Italy

Logical theories of intelligent (or rational) agents have been refined and improved over the past 20 years of research. Such logical theories are used in many ways, one of which is as the basis for executable agent specifications. Here, agents are specified using a logical description and then this description is directly executed in order to implement the agent's behaviour. This provides strong correctness results for the implemented agent, directly corresponding the formal specification with the implementation. With increased application, it has become clear that such specifications of idealised agents are inappropriate in practical situations. An agent may have many resource-bounds to contend with, both in terms of time and memory, and this should be taken into account within the agent's formal specification. Thus, in this paper, we tackle the problem of representing and executing resource-bounded agents. The framework developed here allows the restriction of the amount of reasoning, both temporal and doxastic, that the agent is permitted. We address the formal properties of the framework, present results concerning the execution of such specifications, and consider the practical outcome of such restrictions.

关键词： Formal methods Agent specification Resource-bounded reasoning executable specifications Semantics

来源：评论

学校读者我要写书评

暂无评论

executable specifications for Model-Based Development of Automotive Software

Executable Specifications for Model-Based Development of Aut...

引用

IEEE International Conference on Systems, Man and Cybernetics

作者： Bodenstein, Christoph Lohse, Frank Zimmermann, Armin Tech Univ Ilmenau D-98693 Ilmenau Germany

ISBN: (纸本)9781424465880

Automotive software design is a challenging task because of increasing system complexity. This paper proposes a model-based software development process for complex embedded systems in automotive applications. The gap between early requirement specifications and the development of electronic control units for specific features is bridged with an approach using executable specifications. Behavioral and non-functional properties of the system to be designed can thus be evaluated early during the design process, which improves the confidence of strategic design decisions. Moreover, the executable system model serves as an interface description for module designers, which eases the problem of system integration. The problem of increasing resources for system simulation and optimization is treated by an approach of accuracy adaptive system simulation. The paper presents work in progress towards a complete methodology and tool chain using a CAN bus example.

关键词： adaptive system simulation automotive electronics automotive software design complex embedded systems electronic control units embedded systems executable specifications formal specification model-based development optimisation optimization

来源：评论

学校读者我要写书评

暂无评论

Defect detection for executable specifications - An experiment

引用

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING 2002年第6期12卷 637-655页

作者： Houdek, F Schwinn, T Ernst, D Daimler Chrysler AG Res & Technol D-89013 Ulm Germany Univ Ulm Dept Compiler Construct & Software Engn D-89069 Ulm Germany

The deployment of executable specifications has increased significantly in the last few years. Just as with any other specification documents, these specifications must be examined to ensure the necessary degree of quality. A common and successful technique used for examining traditional specifications is inspection. Now the question has arisen whether inspections on executable specification are the best choice, or if other techniques which use the execution capabilities of the models perform better. In this paper, we empirically compare several defect detection techniques for executable specifications. In particular, we examine inspections, testing, and ad-hoc simulation. Here, we use the specification languages Statemate and Matlab/Simulink. Also, we take a closer look at the inspection process itself and try to quantify the benefits of an inspection meeting for executable specifications.

关键词： executable specifications empirical investigation reviews simulation test

来源：评论

学校读者我要写书评

暂无评论

QUERYING OF executable SOFTWARE specifications

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1992年第8期18卷 705-716页

作者： NOTA, G PACINI, G UNIV VENEZIA DIPARTIMENTO MATEMAT APPL & INFORMATI-30123 VENICEITALY

Several current research efforts in software engineering are investigating executable formal specification languages. The availability of executable specification languages allows testing to be carried out soon after or concurrently with the requirements specification phase. In addition, it becomes possible to use these languages for rapid prototyping, making it possible to gather information on properties of the specified target system including its behavior in response to external events. In this paper, the inspection of software behavior is viewed as the querying of executable specifications. A language RSQ is defined for the purpose of constructing queries against executable specifications expressed in RSF, a language for the description of systems with time constraints. A query is able to single out a subclass of possible behaviors based on properties supplied by the query. The integration of RSQ with RSF enhances the analytical abilities of the software designer and developer.

关键词： BEHAVIOR INSPECTION executable specifications LOGIC SPECIFICATION LANGUAGES RAPID PROTOTYPING STATE TRANSITION RULES

来源：评论

学校读者我要写书评

暂无评论

On the Choice of Models of Computation for Writing executable specifications of System Level Designs 00

On the Choice of Models of Computation for Writing Executabl...

引用

Proceedings of the 13th symposium on Integrated circuits and systems design

作者： I. Jeukens M. Strum

ISBN: (纸本)9780769508436

System level designs are typically heterogeneous, thus combining different technologies. In order to create executable specifications at such a level, a hardware description language, a programming language, or a combination of both is used. However, the resulting description may not be efficient because the ability of each language to capture the system's features is limited by its semantics. This paper presents a methodology for analyzing the efficiency of a set of models of computation to build executable specifications. We defined a set of "behavioral primitives" and evaluated how efficiently they are captured by different models of computation. A debugger/profiler tool was developed. The analysis of the data produced by our tool allows us to derive criteria to choose the most adequate model of computation for each primitive. The analysis of the basic block behavioral primitive is detailed in order to illustrate the method.

关键词： computation models selection CSP program debugging executable specifications communicating sequential processes CAD block behavioral primitive hardware-software codesign codesign debugger/profiler tool behavioral primitives system level designs

来源：评论

学校读者我要写书评

暂无评论

eFLINT: A Domain-Specific Language for executable Norm specifications 2020

eFLINT: A Domain-Specific Language for Executable Norm Speci...

引用

19th ACM SIGPLAN International Conference on Generative Programming - Concepts and Experiences (GPCE)

作者： van Binsbergen, L. Thomas Liu, Lu-Chi van Doesburg, Robert van Engers, Tom Ctr Wiskunde & Informat Amsterdam Netherlands Univ Amsterdam Amsterdam Netherlands Univ Amsterdam Leibniz Inst TNO Amsterdam Netherlands

ISBN: (纸本)9781450381741

Software systems that share potentially sensitive data are subjected to laws, regulations, policies and/or contracts. The monitoring, control and enforcement processes applied to these systems are currently to a large extent manual, which we rather automate by embedding the processes as dedicated and adaptable software services in order to improve efficiency and effectiveness. This approach requires such regulatory services to be closely aligned with a formal description of the relevant norms. This paper presents eFLINT, a domain-specific language developed for formalizing norms. The theoretical foundations of the language are found in transition systems and in Hohfeld's framework of legal fundamental conceptions. The language can be used to formalize norms from a large variety of sources. The resulting specifications are executable and support several forms of reasoning such as automatic case assessment, manual exploration and simulation. Moreover, the specifications can be used to develop regulatory services for several types of monitoring, control and enforcement. The language is evaluated through a case study formalizing articles 6(1)(a) and 16 of the General Data Protection Regulation (GDPR). A prototype implementation of eFLINT is discussed and is available online.

关键词： normative modeling domain-specific language policy enforcement GDPR executable specifications

来源：评论

学校读者我要写书评

暂无评论

specifications ARE (PREFERABLY) executable

引用

SOFTWARE ENGINEERING JOURNAL 1992年第5期7卷 323-334页

作者： FUCHS, NE UNIV ZURICH DEPT COMP SCICH-8057 ZURICHSWITZERLAND

The validation of specifications with respect to user requirements is extremely difficult. To ease the validation task and to give users immediate feedback on the behaviour of the future software, it was suggested that specifications should be made executable. However, Hayes and Jones [1] argue that executable specifications should be avoided because executability can restrict the expressiveness of specification langugages, and can adversely affect implementations. We argue for executable specifications by showing that non-executable formal specifications can be made executable on almost the same level of abstraction, and without essentially changing their structure. No new algorithms have to be introduced to get executability. Furthermore, we show that declarative specification languages combine high expressiveness and executability.

关键词： declarative specification languages formal specification specification languages executable specifications high expressiveness Software engineering techniques expressiveness High level languages non-executable formal specifications user requirements validation task

来源：评论

学校读者我要写书评

暂无评论

Adding liveness to behavioral programming: theory, implementation, and user study

引用

REQUIREMENTS ENGINEERING 2025年 1-23页

作者： Yaacov, Tom Elyasaf, Achiya Weiss, Gera Ben Gurion Univ Negev Beer Sheva Israel

This paper investigates how Behavioral Programming (BP), and executable specifications in general, can more effectively align models with requirements, addressing a key motivation behind BP's development. While BP has traditionally supported safety requirements-defining what a system may, must, and must not do-it lacks direct mechanisms for expressing liveness requirements, which ensure that certain tasks are eventually completed. We introduce a "must-finish" idiom for BP, allowing explicit specification of liveness requirements. We demonstrate how this approach allows for the direct representation of common requirements patterns, supported by a user study that highlights positive outcomes, particularly in improving the alignment between software components and their corresponding requirements. While formal modeling languages that allow specification of liveness requirements are mostly used in the context of model-checking and synthesis, the focus of BP is on the executability of the model. To this end, we propose two execution mechanisms: one based on translation to B & uuml;chi automata and another using Markov decision processes (MDP), with the latter offering scalability through deep reinforcement learning. A formal analysis of the MDP-based mechanism is provided, together with qualitative and quantitative evaluations of a proof-of-concept tool.

关键词： Behavioral programming executable specifications Requirement engineering Liveness

来源：评论

学校读者我要写书评

暂无评论

VASA: An algebra for vague spatial data in databases

引用

INFORMATION SYSTEMS 2010年第1期35卷 111-138页

作者： Pauly, Alejandro Schneider, Markus Univ Florida Dept Comp & Informat Sci & Engn Gainesville FL 32611 USA

Many geographical applications deal with objects in space that cannot be adequately described by determinate, crisp spatial concepts because of their intrinsically indeterminate and vague nature. Geographical information systems and spatial database systems are currently unable to cope with this kind of data. To support the efficient representation, querying, and manipulation of vague spatial data in a database context, we present a formal data model called vague spatial algebra (VASA). This algebra comprises a set of vague spatial data types for vague points, vague lines, and vague regions together with a comprehensive collection of vague spatial operations and vague topological predicates. one of VASA's main benefits is that its formal framework is based on well known, general, and exact models of crisp spatial data types. This enables an exact definition of the vague spatial model since we can build upon an already existing theory of spatial data types. In particular, crisp spatial data types turn out to be a special case of their vague counterparts. In addition, our approach enables executable specifications for the operations, which can be immediately used as implementations. The article offers a precise and conceptually clean foundation for implementing a DBMS extension for vague spatial data and demonstrates the embedding of these new data types as attribute data types in a database schema as well as the incorporation of vague spatial operations and predicates into queries formulated in an SQL-like query language. All concepts have been verified in a prototype implementation. (C) 2009 Elsevier B.V. All rights reserved.

关键词： Vague spatial data types Vague topological predicates Characterization predicates executable specifications Binary constraint networks

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：