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

11th International Workshop on Exploring Modeling Methods for Systems Analysis and Design, EMMSAD 2006 - Held in Conjunction with the 18th Conference on Advanced Information Systems, CAiSE 2006

作者： Ågerfalk, Pär J. Lero - The Irish Software Engineering Research Centre Dept. of Computer Science and Information Systems University of Limerick Ireland Örebro University SE-701 82 Örebro Sweden

Globally distributed software development (GSD) and agile methods are two current and important trends in software and systems engineering. While agile methods seem to cope well with increasingly changing business environments, it is far from obvious how these light-weight processes can best contribute to GSD. In this paper, method rationale is proposed as an analytical tool to understand the values that underpin agile methods and how these map to the GSD domain. Specifically, the paper presents an initial analysis of the values and goals embraced by the 'agile manifesto' and compares briefly with partial results from an ongoing study on the use of agile methods in GSD.

关键词： software design

来源：评论

学校读者我要写书评

暂无评论

Specification matching of object-oriented components

Specification matching of object-oriented components

引用

International Conference on software engineering and Formal Methods (SEFM)

作者： F. Feiks D. Hemer Institute for Software Engineering and Theoretical Computer Science Technical University Berlin Germany Software Verification Research Centre School of Information Technology and Electrical Engineering University of Queensland Australia

Object-orientation supports software reuse via features such as abstraction, information hiding, polymorphism, inheritance and redefinition. However, while libraries of classes do exist, one of the challenges that still remains is to locate suitable classes and adapt them to meet the specific requirements of the software developer. Traditional approaches to library retrieval are text-based; it is therefore difficult for the developer to express their requirements in a precise and unambiguous manner. A more promising approach is specification-based retrieval, where library component interfaces and requirements are expressed using a formal specification language. In this case retrieval is based on matching formal specifications. In this paper, we describe how existing approaches to specification matching can be extended to handle object-oriented components.

关键词： software libraries Formal specifications software engineering Information retrieval computer science Information technology Specification languages

来源：评论

学校读者我要写书评

暂无评论

An introduction to real-time object-Z

An introduction to real-time object-Z

引用

作者： Smith, Graeme Hayes, Ian Software Verification Research Centre University of Queensland Brisbane QLD Australia School of Computer Science and Electrical Engineering University of Queensland Brisbane QLD Australia Software Verification Research Centre University of Queensland Brisbane QLD 4072 Australia

This paper presents Real-Time Object-Z: an integration of the object-oriented, state-based specification language Object-Z with the timed trace notation of the timed refinement calculus. This integration provides a method of formally specifying and refining systems involving continuous variables and real-time constraints. The basis of the integration is a mapping of the existing Object-Z history semantics to timed traces. © 2002 BCS.

关键词： computer hardware description languages

来源：评论

学校读者我要写书评

暂无评论

Refinement calculus for logic programming in Isabelle/HOL 14th

Refinement calculus for logic programming in Isabelle/HOL

引用

14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001

作者： Hemer, David Hayes, Ian Strooper, Paul Software Verification Research Centre The University of Queensland Australia School of Computer Science and Electrical Engineering The University of Queensland Australia

ISBN: (纸本)354042525X

This paper describes a deep embedding of a refinement calculus for logic programs in Isabelle/HOL. It extends a previous tool with support for procedures and recursion. The tool supports refinement in context, and a number of window-inference tactics that ease the burden on the user. In this paper, we also discuss the insights gained into the suitability of different logics for embedding refinement calculii (applicable to both declarative and imperative paradigms). In particular, we discuss the richness of the language, choice between typed and untyped logics, automated proof support, support for user-defined tactics, and representation of program states. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Logic programming

来源：评论

学校读者我要写书评

暂无评论

Using theory interpretation to mechanise the reals in a theorem prover

Using theory interpretation to mechanise the reals in a theo...

引用

Computing: The Australasian Theory Symposium (CATS 2001)

作者： Shield, Jamie Hayes, Ian Carrington, David Software Verification Research Centre University of Queensland 4072 Australia School of Computer Science and Electrical Engineering University of Queensland 4072 Australia

The mechanisation of the real numbers within theorem provers is of practical benefit for the verification of real-time systems. The real numbers provide a foundation within the theorem prover for classical mathematical analysis such as differentiation and integration. The approach we have taken makes extensive use of the theory interpretation facilities of the interactive theorem prover Ergo to maximise theory reuse and hence minimise theorem redundancy. The theory developed is compared with Harrison's HOL version. © 2001 Published by Elsevier science B.V.

关键词： Theorem proving

来源：评论

学校读者我要写书评

暂无评论

Using Theory Interpretation to Mechanise the Reals in a Theorem Prover

引用

Electronic Notes in Theoretical computer science 2001年 42卷 266-281页

作者： Jamie Shield Ian Hayes David Carrington Software Verification Research Centre The University of Queensland Australia 4072 School of Computer Science and Electrical Engineering The University of Queensland Australia 4072

关键词：

来源：评论

学校读者我要写书评

暂无评论

Animation can show only the presence of errors, never their absence

Animation can show only the presence of errors, never their ...

引用

Australian Conference on software engineering

作者： T. Miller P. Strooper School of Computer Science and Electrical Engineering Software Verification Research Centre University of Queensland Brisbane QLD Australia

A formal specification animator executes and interprets traces on a specification. Similar to software testing, animation can only show the presence of errors, never their absence. However, animation is a powerful means of finding errors, and it is important that we adequately exercise a specification when we animate it. The paper outlines a systematic approach to the animation of formal specifications. We demonstrate the method on a small example, and then discuss its application to a non-trivial, system-level specification. Our aim is to provide a method for planned, documented and maintainable animation of specifications, so that we can achieve a high level of coverage, evaluate the adequacy of the animation, and repeat the process at a later time.

关键词： Animation Formal specifications Specification languages computer errors software testing Concrete computer science Australia Documentation Guidelines

来源：评论

学校读者我要写书评

暂无评论

Combining the animation and testing of abstract data types

Combining the animation and testing of abstract data types

引用

Asia-Pacific Conference on Quality software

作者： T. Miller P. Strooper School of Computer Science and Electrical Engineering Software Verification Research Centre University of Queensland Brisbane QLD Australia

ISBN: (纸本)0769512879

A formal specification animator interprets and executes specifications to give them the appearance of liveliness. This can be used to identify errors in a specification because it provides concrete examples of the behaviour of the specification. By providing a suitable user interface, it allows users unfamiliar with specification languages and notations to interact with the specification. We exploit the similarities between animation and testing, and present a method that combines specification animation and software testing of abstract data types (ADTs). Tool support is provided by Peach, which supports the animation of a specification and the testing of an implementation of that specification. We demonstrate the use of our method and tool on a small example, and discuss its application to a larger example.

关键词： Animation Formal specifications software testing computer science Australia computer errors Concrete User interfaces Application software Life testing

来源：评论

学校读者我要写书评

暂无评论

Testing Java monitors through deterministic execution

Testing Java monitors through deterministic execution

引用

Australian Conference on software engineering

作者： C. Harvey P. Strooper School of Computer Science and Electrical Engineering Software Verification Research Centre University of Queensland Brisbane QLD Australia

Java is a popular, modern programming language that supports monitors. However, monitor implementations, like other concurrent programs, are hard to test due to the inherent non-determinism. The paper presents a method for testing Java monitors, which extends the work of P. Brinch Hansen (1978) on testing Concurrent Pascal monitors. A monitor is tested by executing a concurrent program in which the processes are synchronised by a clock to make the sequence of interactions deterministic and reproducible. The method is extended to account for the differences between Concurrent Pascal monitors and Java monitors, and to provide additional coverage of the implementation under test. Tool support and documentation in the form of a test plan are also provided. The method is illustrated in detail on an asymmetric producer-consumer monitor, which is the same example that was used to illustrate the original method. The application of the method to the readers and writers problem is also discussed.

关键词： Testing Java computer displays Clocks Australia Synchronization Documentation computer science Modems computer languages

来源：评论

学校读者我要写书评

暂无评论

Systematically deriving partial oracles for testing concurrent programs

Systematically deriving partial oracles for testing concurre...

引用

Australasian computer science Conference

作者： C. Hunter P. Strooper School of Computer Science and Electrical Engineering Software Verification Research Centre University of Queensland Brisbane QLD Australia

ISBN: (纸本)0769509630

The problem of verifying the correctness of test executions is well-known: while manual verification is time-consuming and error-prone, developing an oracle to automatically verify test executions can be as costly as implementing the original program. This is especially true for concurrent programs, due to their non-determinism and complexity. In this paper, we present a method that uses partial specifications to systematically derive oracles for concurrent programs. We illustrate the method by deriving an Ada task that monitors the execution of a concurrent Ada program and describe a prototype tool that partially automates the derivation process. We present the results of a study that shows the derived oracles are surprisingly effective at error detection. The study also shows that manual verification is an inaccurate means of failure detection, that large test case sets must be used to ensure adequate testing coverage, and that test cases must be run many times to cover for variations in run-time behaviour.

关键词： System testing Automatic testing software testing Prototypes Runtime Costs Formal specifications computer science Australia computer errors

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：