- 41
- Kamel Boumaza, UNU-IIST
15:00 - 16:00, Friday 14 December 2007
Title: Formal Analysis of Timed Asynchronous Circuit Behaviours
Abstract:
Designing asynchronous circuits can avoid various problems
which arise in the design of synchronous circuits, such as clock skew and high power consumption. Unfortunately asynchronous circuits exhibit the serious
problem of "hazard". In this talk we will explain how can we model and
detect hazards in timed asynchronous circuits using signal and event models.
Circuit behaviours are modelled as timed automata: each gate in the circuit
is modelled as an automaton, and by using the UPPAAL model checker, can be
verified for deadlock which can be made to reflect exactly the phenomena of
a hazard.
- 40
- Nyamdorj Ganbold, Center for Electronic Governance at UNU-IIST, Information and Communication Technology Authority The Government of Mongolia
11:30, Friday, 14 December 2007
Title: Electronic Government in Mongolia - Status, Challenges, Recommendations
Abstract:
The aim of this seminar is to present the context and status
of Electronic Government development in Mongolia, identify existing
challenges and offer some recommendations on how to overcome them. The
status will consider various dimensions of Electronic Government
development - political, regulatory, organizational, human, financial,
technological and infrastructural. It will also consider data,
services, communication and collaboration. A few examples of concrete
initiatives will be presented to illustrate the ongoing development,
working across these dimensions as well as agency and sectoral
(public-private) boundaries. The examples will highlight the
challenges acting against Electronic Government development in
Mongolia, and illustrate possible ways to overcome them by selecting
and adapting internationally recognized best practices to local
conditions. The seminar will conclude by exploring various scenarios
for collaboration between the Information and Communication Technology
Authority and the Center for Electronic Governance at UNU-IIST to help
implement some of these recommendations.
- 39
- Bimal Pratap Shah, Center for Electronic Governance at UNU-IIST, National Information Technology Center Ministry of Environment, Science and Technology The Government of Nepal
11:00, Friday, 14 December 2007
Title: Electronic Government in Nepal - Status, Challenges, Recommendations
Abstract:
The aim of this seminar is to present the context and status
of Electronic Government development in Nepal, identify existing
challenges and offer some recommendations on how to overcome them. The
status will consider various dimensions of Electronic Government
development - political, regulatory, organizational, human, financial,
technological and infrastructural. It will also consider data,
services, communication and collaboration. A few examples of concrete
initiatives will be presented to illustrate the ongoing development,
working across these dimensions as well as agency and sectoral
(public-private) boundaries. The examples will highlight the
challenges acting against Electronic Government development in Nepal,
and illustrate possible ways to overcome them by selecting and
adapting internationally recognized best practices to local
conditions. The seminar will conclude by exploring various scenarios
for collaboration between the National Information Technology Center
and the Center for Electronic Governance at UNU-IIST to help implement
some of these recommendations.
- 38
- Einar Broch Johnsen, University of Oslo
11:00, Friday, 7 December 2007
Title: Creol: Modeling Reconfigurable Distributed Concurrent Objects
Abstract: In this talk, we give an overview of Creol, an object-oriented modeling
language developed in the CREDO project. Creol is an executable, formally
defined modeling language targeting open distributed systems. We highlight
how the language deals with distribution and openness through asynchronous
method calls, futures, and runtime class updates, and give some intuitions
about its operational semantics and type system.
Biography:
Einar Broch Johnsen is associate professor at the University of Oslo. His
PhD (2002) was on formal viewpoint specification of open distributed
systems. In addition to object orientation and open systems, his research
interests include formal systems and methods such as rewriting logic, proof
systems, type theory, and theorem proving.
- 37
- Frank S. de Boer, CWI, Amsterdam
11:00, Thursday, 29 November 2007
Title: Tasks for Actors in the Credo project
Abstract:
The presentation starts with a discussion of the overall objectives and
workplan of the EU Credo project on modeling and analysis of evolutionary
structures for distributed services.
As an example of the work carried out in the project I will introduce the
formalism of task automata for the specification and analysis
of scheduling policies in actor-based programming languages.
Biography:
I did my PhD research a the CWI and obtained my PhD degree in 1991.
In my thesis (1991) reasoning about dynamically evolving process
structures (A proof theory of the parallel object-oriented language POOL)
I developed a first sound and complete proof method for a (parallel)
object-oriented language, designed and implemented at Philips Research
Laboratories in the context of an EU ESPRIT project.
Currently, I'm working as senior researcher at the CWI in the
research group on coordination languages.
Other current affiliations are the Leiden Institute of Advanced
Computer Science (LIACS) and Utrecht University (UU).
- 36
- Jan Rutten, CWI and VU, Amsterdam
11:00, Thursday, 22 November 2007
Title: Linear systems, coalgebraically
Abstract: Linear systems are simple state-based systems,
mostly studied in systems and control theory,
and not so much in computer science.
Linear systems offer a basic but interesting
model of memory and feedback, and serve as
representations of (functions on) streams
(infinite sequences). As rational languages correspond
to finite automata, rational streams correspond to
finite dimensional linear systems.
Computationally, this amounts to systems with
feedback and finite memory.
Coalgebra is a general framework for
describing dynamical systems in general, and
infinite data structures in particular.
The notion of coalgebra is in a precise sense
a formal dual to the notion of algebra.
The set of natural numbers is a fundamental example of
an (initial) algebra. Similarly, the set of
streams is a canonical example of a (final) coalgebra.
In this talk, we shall describe the semantics of linear systems
exploiting the finality of the coalgebra of streams.
This leads to an easy computation of representations
of rational streams.
Slides of this talk and a related paper can be found at:
http://homepages.cwi.nl/ janr/papers/
Reference:
J.J.M.M. Rutten.
Coalgebraic foundations of linear systems (an exercise in stream
calculus). Proceedings CALCO 2007, LNCS 4624, Springer, 2007, pp. 425-446.
- 35
- Prof. Ursula Martin, Queen Mary, University of London, UK
15:00, Friday, 9 November 2007
Title: Design Verification for Control Engineering
Abstract: In the first part of this talk I'll introduce control engineering
as a new domain of application for formal methods. I'll discuss
design verification, drawing attention to the role played by
diagrammatic evaluation criteria involving numeric plots of a
design, such as Nichols and Bode plots. I'll show that symbolic
computation and computational logic can be used to discharge
these criteria and provide symbolic, automated, and very general
alternatives to these standard numeric tests, and illustrate our
work with reference to a standard reference model drawn from
military avionics.
At the heart of this work is the observation that control systems
based on linear differential equations exhibit "program-like"
phenomena such as loops and sequential composition, which allows
the development of a Hoare-style logic. While trying to understand
this phenomenon we hit upon a new abstract presentation of Hoare
Logic based on categories with feedback, which can also be used
to capture extensions of the standard Hoare logic for while
programs, e.g. the extension with pointer manipulations via
separation logic.
The work has been funded by Qinetiq, Intel and the Engineering and Physical
Sciences Research Council.
References:
Richard Boulton, Hanne Gottliebsen, Ruth Hardy, Tom Kelsey & Ursula Martin,
Design Verification for Control Engineering. Integrated Formal Methods,
4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004,
Lecture Notes in Computer Science vol 2999, pages 21-35, Springer, 2004.
Ursula Martin, Erik Mathiesen and Paulo Oliva, Hoare Logic in the Abstract.
Proceedings of Computer Science Logic Conference 2006. Lecture Notes in
Computer Science vol 4207, pages 501-515, Springer, 2006.
Biography:
Ursula Martin is a British computer scientist. She is Vice-Principal of Science
and Engineering at Queen Mary, University of London and a Professor of Computer
Science in the Department of Computer Science there.
Ursula Martin gained an MA from the University of Cambridge and a PhD from the
University of Warwick, both in mathematics. She has held academic posts at
University of Illinois at Urbana-Champaign (U.S.), the University of Manchester
(UK), Royal Holloway, University of London She has made sabbatical visits to
MIT and SRI International (Menlo Park).
From 1992 to 2002, she was Professor of Computer Science at the University of
St Andrews in Scotland. She was the first female professor at the University
since its foundation in 1411.
From 2003 to 2005, Ursula Martin was seconded to the University of Cambridge
Computer Laboratory part-time as Director of the Women@CL project to lead
local, national and international initiatives for women in computing, supported
by Microsoft Research and Intel Cambridge Research. She was a Fellow of Newnham
College, Cambridge.
She is Advisory Editor for the Annals of Pure and Applied Logic journal
(published by Elsevier) and on the editorial boards for The Journal of
Computation and Mathematics (London Mathematical Society) and Formal Aspects of
Computing (Springer-Verlag).
Throughout Ursula Martin's career, she has been involved in many activities
aimed at encouraging women in the fields of computing and mathematics. Her
research interests have been in the area of theoretical computer science and
formal methods.
- 34
- Charles Morisset, UNU-IIST
11:00, Friday, 2 November 2007
Title: Formalisation and Comparison of Access Control Policies
Abstract: One of the aspects of computer security relates to the control of
the access to the data of a system for which various security policies
can be enforced. However, it is useless to set up a security policy if
the programs enforcing such a policy are not sound. Hence, we use formal
methods to deal with access control. I introduce an abstract semantical
framework allowing for the specification, the implementation and the
comparison of access control policies and instantiate it with well-known
access control policies such as Bell and LaPadula, The Chinese Wall and
RBAC.
- 33
- Professor Grigoris ANTONIOU, Department of Computer Science,
University of Crete, Greece and Head of the Information Systems Laboratory at FORTH
11:00, Friday, 19 October 2007
Title: Ontology Evolution on the Semantic Web
Abstract: The evolution of knowledge has been studied for decades in the area of
knowledge representation and reasoning. This line of work, known as
belief revision, has produced many and deep results. The emergence of
the semantic web initiative, and the associated increase in the use of
ontologies on the Web, has created new interest in this problem, driven
by specific application needs in areas, such as digital preservation and
e-learning.
As we will explain in this talk, the problem of ontology evolution can
benefit from ideas from belief revision, but needs to address new
challenging issues. After describing the general problem, we will
proceed to present an ongoing work on revising RDF ontologies.
Biography:
Grigoris Antoniou is Professor of Computer Science at the University of
Crete, Greece, and Head of the Information Systems Laboratory at FORTH,
the top-rated Greek research institute involved in many European
projects. Before joining FORTH, he held professorial positions at
Griffith University, Australia, and the University of Bremen, Germany.
His research interests lie in knowledge representation and reasoning,
and its applications to the semantic web, e-commerce, digital
preservation and ambient intelligence. He has published over 150
technical papers in scientific journals and conferences. He is author of
three books with prestigious international publishers (Addison-Wesley
and MIT Press); his book "A Semantic Web Primer" is the standard
textbook in this area. He participates in a number of research projects,
among them the European projects REWERSE (reasoning on the web) and
CASPAR (digital preservation). In 2006 he was elected ECCAI Fellow,
joining the prestigious list of the top European researchers in
artificial intelligence.
- 32
- Dimitar P. Guelev, Institute of Mathematics and Informatics, Bulgarian Academy of Sciences
15:00, Friday, 7 September 2007
Title: A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic
Abstract: We present a new proof of the fact that every formula in discrete time
linear temporal logic with past is equivalent to a conjunction of formulas
of the form
<>[] A=> <>[] B
where A and B are past formulas. This form is known as the general canonical
reactivity form. The original proof is based on the fact that a finite
automaton recognizes an LTL-definable omega-language iff it is counter-free
(a result from Lenore Zuck's thesis in 1986) and relies on the theorem of
Krohn-Rhodes about cascade decomposition of finite automata. A shorter proof
was outlined by Mark Reynolds in 2000. That proof involved adding an
infinity time point to the discrete flow of time and syntactical
transformations using separation for Dedekind-complete time.
The new proof involves only equivalence transformations and makes use of
Gabbay's separation theorem for the standard discrete flow of time. This
theorem has a proof that is based on equivalence transformations too.
Therefore the new proof entails an algorithm to obtain the canonical form
without resorting to constructions outside discrete time LTL with past
operators such as automata.
- 31
- Dr Paolo Zuliani, University of Oxford
15:00, Friday, 24 August 2007
Title: Reasoning about faulty quantum programs
Abstract: We present a formalism for reasoning about errors in quantum
computation.
In particular, we treat errors in quantum measurements using a
quantum programming language. We apply our model to Bell's
experiment (also known as Bell inequalities), a fundamental
result in quantum mechanics and a tool for detecting eavesdropping
in quantum cryptography protocols.
We code Bell's experiment as a program with faulty measurements,
and we derive lower bounds for the efficiency of the measurement
devices. No previous knowledge of quantum mechanics is assumed,
though we shall use some basic concepts of vector spaces.
Biography:
Paolo is visiting UNU-IIST for a week to work on quantum computing
with JWS. He holds a Marie-Curie International Postdoctoral
Scholarship and is interested in formal methods and quantum
computation. He has a PhD from the University of Oxford (2001) since
when he has worked at the Universities of Bolzano (Italy) and
Princeton (USA).
See http://web.comlab.ox.ac.uk/oucl/work/paolo.zuliani/
- 30
- Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
11:15, 9 August 2007
Title: Mondex (2)
Abstract:
- 29
- Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
10:00, 9 August 2007
Title: Mondex (1)
Abstract:
- 28
- Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
11:15, 8 August 2007
Title: Examples of Verification with OTS/CafeOBJ
Abstract:
- 27
- Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
10:00, 8 August 2007
Title: OTS (Observational Transition Systems)
Abstract:
- 26
- Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
11:15, 7 August 2007
Title: Basics of CafeOBJ (including proof score)
Abstract:
- 25
- Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
10:00, 7 August 2007
Title: Introduction to CafeOBJ
Abstract:
- 24
- Florian Kammueller, T U Berlin
15:00, 27 July 2007
Title: Adapting Safely - HOL Theorem Proving applied to Aspect-Orientation
Abstract: In order to provide safe aspects for adaptive systems we address the
verification of the aspect-oriented language paradigm. We construct a
formalization of a basic calculus for aspects in Isabelle/HOL. This talk
presents the following contributions:
(a) an adequate formalization of the ς-calculus in Isabelle/HOL
(b) a type system for this theory of objects including the proof of type
safety and confluence, and
(c) a new concept of a theory of yaspects based on the theory of objects
including a type system.
Finally the impact of this work on the analysis of the calculus of
distributed objects ASP is summarized and future work is discussed.
- 23
- Tiziana Margaria, University of Potsdam
11:00, 19 July 2007
Title: Services: from telecommunications to the web
Abstract:
- 22
- Bernhard Steffen, University of Dortmund
10:00, 19 July 2007
Title: Learning in Practice: test based discovery of behavioural models
Abstract:
- 21
- Professor Teodor C. Przymusinski, University of California at Riverside
11:00, Monday, 16 July 2007
Title: Updating Knowledge Databases
Abstract: We are continuously faced with the need to update the knowledge
that we possess. Performing updates allows us to learn new facts
and discard those that no longer hold. One can reasonably argue
that most, if not all, of our knowledge is acquired via suitable
sequences of updates. By extension, the same applies to intelligent
artifacts, such as intelligent knowledge bases and intelligent agents.
We will describe an approach to knowledge updates based on the
so-called interpretation updates. We will show how a version of
Newton's principle of inertia can be used to provide an elegant
characterization of such updates. Our approach extends and simplifies
the notions of revision programs and the notion of a formula update,
introduced earlier by W. Marek and M. Truszczynski and by M. Winslett,
respectively. This presentation is based on the joint paper with
Hudson Turner.
- 20
- Yang Lu, UNU-IIST Fellow
15:00, Friday, 20 July 2007
Title: Correctness preserving transformations in MDA
Abstract: We propose a semi-automatic transformation-based approach of
developing a component-based model from an object-oriented model. The
transformation is expected to preserve the semantics and specified
properties of the source model. We will show how rCOS can be integrated into
the object-oriented and component-based development process and give formal
support for correctness preserving transformations. The transformation is
implemented in the relational language of Query/View/Transformation (QVT)
standardized by OMG.
- 19
- Yongmei Liu, Hong Kong University of Science and Technology
15:00, Friday, 29 June 2007
Title: Tractable Reasoning in Incomplete First-order Knowledge Bases
Abstract: One of the most important yet elusive goals in the area of Knowledge
Representation is to devise a general-purpose, semantically motivated,
and computationally tractable reasoning service. We propose a general
methodology to establish tractable reasoning services for incomplete
first-order knowledge bases. It consists of defining a logic that is
weaker than classical logic and has two properties: first, the entailment
problem can be reduced to the model checking problem for a certain
characteristic model; and second, the model checking problem is
tractable for formulas with a bounded number of variables. We
apply this methodology to two forms of incomplete first-order
knowledge bases: one for open-world reasoning, that is, the
knowledge base is equivalent to a possibly infinite set of ground
literals, and the other for reasoning with disjunctive information.
This is joint work with Hector Levesque and Gerhard Lakemeyer.
- 18
- Hong Zhu, Department of Computing, Oxford Brookes University, UK
15:00, Friday, 22 June 2007
Title: Towards a Scenario Calculus for Formal Reasoning of Emergent Behaviours of Multi-Agent Systems
Abstract: Emergent behaviour is a common phenomena in multi-agent systems in which
autonomous agents perform actions with only limited access to local
information and making decisions individually; meanwhile the whole system
demonstrates properties and behaviours that have strong global features.
A typical example of the applications of emergent behaviours is the
self-organisation of autonomous agent communities. Because of the huge gap
between individual agentsproperty and behaviour and those of the whole
system, specifying and reasoning about emergent behaviours are notoriously
difficult if not impossible. In this talk, I will report a recent attempt
in the development of a formal theory, which is called scenario calculus,
for logical analysis and formal proofs of emergent behaviours in
multi-agent systems. The theory will be illustrated by examples including
autonomous sorting and a variety of self-organised agent communities.
Biography:
Dr. Hong Zhu is a professor of computer science at Oxford Brookes
University, where he chairs the applied formal methods group. Prof. Zhu
obtained his BSc, MSc, PhD degrees in Computer Science from Nanjing
University, China, in 1982, 1984 and 1987, respectively. He was with
Nanjing University after obtained his PhD degree in Sept. 1987. From
October 1990 to December 1994, he was a research fellow at Brunel
University and the Open University, UK. He returned to Nanjing University
in Dec. 1994 and joined Department of Computing of Oxford Brookes
University in November 1998.
Prof. Zhus research interests are in the area of software engineering
including software development methodology, software testing, agent
technology, automated software development tools, etc. He has published
more than one hundred research papers and two books. He has won a number
of prizes in China for his research achievements, which include the
Premiers Award of Distinguished Young Scientists in China awarded by the
National Natural Science Foundation of China in 1997 and Ho YingDong Prize
of Research Achievement (second prize) awarded by Ho YingDong Foundation
of the Ministry of Education of China in 1992, and Cheung Kong Scholar
Professorship of the Ministry of Education of China in 2000.
- 17
- Choe Changil
15:45, Monday, 28 May 2007
Title: On Verification of Linear Occurrence Properties of Real-Time Systems
Abstract: Duration Calculus of Weakly Monotonic Time (WDC) is an
extension of DC to allow description of discrete processes where
several steps of computation can occur at the same time point. In
this paper, we introduce Linear Occurrence Invariants (LOI) which
is a subclass of WDC formulas and give an algorithm to check
real-time automata for LOI using integer programming. LOI can be
used effectively to specify system requirements in some cases
including when the system is considered under the true synchrony
assumption. We also extend WDC probabilistically to express
dependability requirements of real-time systems and develop
techniques to check deterministic probabilistic real-time automata
for a class of probabilistic WDC formulas.
- 16
- Tran Thi Bich Hanh
15:00, Monday, 28 May 2007
Title: Verification of an Air-Traffic Control System with Probabilistic Real-time Model-checking
Abstract: In this paper we present an approach to safety verification of Air-Traffic
Control Systems (ATC) using probabilistic timed model-checking. Namely we
use ATC as a case study for formal analysis of real time systems whose
performance depends on uncertain or probabilistic behaviors. We construct
a probabilistic timed automata model for ATC by extending the Operator
Choice Model (OCM), a model of operators' behaviors in ATC system, with
timed and probabilistic assumptions. Some properties of this system are
then expressed in probabilistic real time computation tree logic (PCTL).
The verification results produced by using the tool PRISM illustrate the
uses of this approach to better understand the human errors in real time
systems.
- 15
- Jong Hyo Jin
15:00, Friday, 25 May 2007
Title: Specifying and Verifying Multicast Communication Protocols
Abstract: In this work, we study about formal design and verification of protocols
using CSP (Communicating Sequential Processes) formalism.
The protocols concern multicast communications; we develop formal models
of multicast communication protocols with CSP and then verify the models
using FDR which is the model checking tool of CSP.
- 14
- Rudi Schlatte
15:00, Friday, 18 May 2007
Title: Testing and Formal Methods
Abstract: Testing and Formal Methods have grown closer together in recent years.
In general, testing is a way to find errors in a system implementation
by means of experimenting with it. Although formal methods original aim is
to prove that a system is
correct, their recent applications to industrial case studies have
shown that they are also very effective when they are used to find
errors. In particular, when we are using formal methods to develop
a system, the artifacts thereby created can be used to generate
test cases for the resulting implementation. I will present some
scenarios and techniques of how to generate test cases from a formal
specification.
- 13
- Ying Mingsheng, Tsinghua University, China
15:00, Friday, 11 May 2007
Title: Quantum Loop Programs
Abstract: Loop is a powerful program construct in classical computation, but
its power is still not exploited fully in quantum computation. The
exploitation of such power definitely requires a deep understanding
of the mechanism of quantum loop programs. In this paper, we
introduce a general scheme of quantum loops and describe its
computational process. The notions of termination and almost
termination are proposed for quantum loops, and the function
computed by a quantum loop is defined. To show their expressive
power, quantum loops are applied in describing quantum walks.
Necessary and sufficient conditions for termination and almost
termination of a general quantum loop on any mixed input state are
presented. A quantum loop is said to be (almost) terminating if it
(almost) terminates on any input state. We show that a quantum loop
is almost terminating if and only if it is uniformly almost
terminating. It is observed that a small disturbance either on the
unitary transformation in the loop body or on the measurement in the
loop guard can make any quantum loop (almost) terminating. Moreover,
a representation of the function computed by a quantum loop is given
in terms of finite summations of matrices. To illustrate the notions
and results obtained in this paper, two simplest classes of quantum
loop programs, one qubit quantum loops, and two qubit quantum loops
defined by controlled gates, are carefully examined.
BIO: Mingsheng Ying was born in Jiangxi, in 1964. He graduated from the
Department of Mathematics, Fuzhou Teachers College, in 1981. He is
currently Cheung Kong Professor at the State Key Laboratory of Intelligent
Technology and Systems, Department of Computer Science and Technology,
Tsinghua University, and Chairman of the Association of Fuzzy Systems and
Mathematics of China. He is in the Editorial Board of Fuzzy Sets and
Systems. His research interests include semantics of programming, logic in
computer science and artificial intelligence, quantum computation, and
fuzzy logic. He has published more than 60 papers in various journals,
e.g., Journal of Symbolic Logic, Theoretical Computer Science, Artificial
Intelligence, IEEE Transactions on Fuzzy Systems. He also published a
research monograph Topology in Process Calculus: Approximate Correctness
and Infinite Evolution of Concurrent Programs (Springer-Verlag, New York,
2001).
- 12
- Andreas Griesmayer
15:00, Friday, 4 May 2007
Title: Debugging Software: from Verification to Repair
Abstract:
I will talk about the main topics of my PhD Thesis, where I used and
extended model checking techniques to localize and repair faults in
software.
If model checker finds out that a program does not fulfill its
specification, it delivers a counterexample, a run which demonstrates
the wrong behavior. Even with a counterexample, locating the actual
fault in the source code is often a difficult task for the programmer.
Fault localization reduces the set of statements that have to be
examined manually by the programmer. I will present an automated
approach for fault localization and its application to C programs.
The "next step" in the debugging cycle, after finding the position of a
fault, is to find an alternative implementation for a statement that
removes the error. To this end, it is not enough to look
at one counter example, we have to ensure that the new implementation
fulfills the specification in all possible runs on the program.
To be able to do this, we use abstraction to map the C program to a
Boolean program. We fix faults in the Boolean program by extending it to
a game, in which the protagonist (the "good guy", the system) can select
an alternative implementation for an incorrect statement, while the
antagonist (the "evil guy", the environment) tries to find input values
to provoke an error. If the protagonist can can find a strategy to
avoid the error no matter what the antagonist does, we have found a
correction for the Boolean program. The abstract repair is mapped back
to C and used to suggest a repair for the programmer.
The talk will also scratch the topics of abstraction refinement (CEGAR)
and pushdown systems. (Boolean programs support function calls and
therefore infinite state-space, which is not representable in "normal"
finite state automata.)
- 11
- Wang Xu
11:00, Friday, 27 April 2007
Title: Two case studies of asynchronous circuit verification
Abstract: This talk uses two case studies to illustrate, step by step, the obstacles
we will be facing in model-checking systems from the real world. The steps
include understanding the problem, model building, and avoiding state
space
explosion. It draws on my past experience of using CSP/FDR to verify
asynchronous circuits. We will see how we can successfully verify a
distributed coloring algorithm for asynchronous pipeline processor
(high-level) and a fragment of circuits implementing handshake component
(low level), despite these difficulties.
The talk will be useful to (quite a few) staffs and fellows who are now
using CSP/FDR2 to verify their respective problems.
- 10
- Paddy Krishnan, Bond University, Australia
15:00, Wednesday, April 25 2007
Title: An Activity Based Technique to Increase Interest in Computer Activity
Abstract:
Most of the high school curricula for computer science focus
only on the application and technical aspects such as the use of
wordprocessing, spreadsheeting, and programming. This reinforces the view
that Computer Science is an activity that involves tinkering with
computers.
I will demonstrate a few ideas on how certain activities can be used to
increase an awareness in the science of computation. These activities are
essentially algorithmic problem solving but without the jargon and
technical details. I have used them at a local high school with some
success.
This is an informal seminar and I hope to involve the audience to both
solve the problems and also give feedback on the approach.
- 9
- Chris George
15:00, Friday, April 20 2007
Title: Specification, Model Checking, and Proof of the Mondex Electronic
Purse
Abstract: The Mondex Electronic Purse was originally specified in Z and proved
correct manually in 2000. It has since been used as a challenge problem
for automatic correct development, as part of the Grand Challenge for
developing correct software. We describe the specification of Mondex in
the RAISE specification language and arguments for its correctness using
both model checking and proof using the RAISE tools, and look at the
problems involved. (The material
on model checking has been added since an earlier version of this seminar
was presented, about a year ago.)
- 8
- Yifeng Chen, UNU-IIST visitor, from Durham University, UK
13:00, Friday, 13 April 2007
Title: Compositional Reasoning for Pointer Structures
Abstract: This paper studies the compositional definition and behaviour of
properties that arise in pointer structures. A pointer structure is
represented as a (pointer) graph. A pointer property is a set of
pointer structures. A parameterised binary combinator is defined
that enables important properties (like acyclicity, canonicity and
reachability) to be defined in a compositional manner. The technique
of parameterising a combinator derives from the definition of
parallel-by-merge in `Unifying Theories of Programming'. It is
applied here to the study of disjointness combinators that extend
the separating conjunction of Separation Logic. A case study is
provided to demonstrate how these ideas are used, in the form of
rules of Hoare logic, to verify the correctness of an
Object-Oriented program.
IMPORTANT ADDITIONAL ANNOUNCEMENT:
Following the seminar, at something like 4:30, there will be
drinks (and a very brief tutorial introduction to wine tasting
though of course there will be nonalcoholic drinks too) in the
UNU-IIST roof garden.
- 7
- Paddy Krishnan, Professor and Head of Department Software Systems
10:00 - 12:00, Thursday, 12, 19 April 2007
Title: Understanding Model Based Testing
Abstract:
Aims: The aim of this course is
a) to introduce the participants to some of the aspects of model based
testing using a commercial tool
b) understand the limitations/strengths of model based testing and
c) identify potential improvements to the process.
The course will run as a "practical hands on course". The commercial tool
is available as a Virtual Machine (VMWare). Participants can install it
and play around with it. I will give an initial lecture to guide the
process and will be available for consultation etc. I expect each
participant to spend about 12-15 hours on the topic. At the end of topic,
people have to present their findings in an informal setting.
- 6
- Jeff Sanders, UNU-IIST
15:00, Friday, 6 April 2007
Title: What I do
Abstract: Now that I've (almost) settled in at UNU/IIST it's time to
present a seminar explaining the themes behind my
work and the topics that interest me. This gentle talk
has been designed to be intelligible to all. Please come
along and ask questions.
- 5
- Young Sik (YS) Kim, Korean International Cooperation Agency
(KOICA), eGovernment Advisor, National Information Technology Center,
Government of Nepal
16:00 - 17:30, Wednesday, 14 March 2007
Title: Developing ICT and Electronic Government in Developing
Countries - Experiences from the Republic of Korea
Abstract: The Republic of Korea (RoK) is supporting developing
countries in raising the level of their Information and Communication
Technology (ICT) and Electronic Government. During the last five to
six years, the RoK was engaged in many ICT and Electronic Government
development projects through grants or soft loans offered to
developing countries. I have been directly engaged since 2005 in one
of these projects - the development of the Electronic Government
Master Plan (eGMP) for the Government of Nepal. This seminar will
present the eGMP Project - history, content, next steps and lessons
learnt. I will also introduce other cases of international cooperation
in ICT and Electronic Government development between the RoK and
various developing countries, through the general cooperation
structure established by the RoK Government.
TARGET AUDIENCE: Government officials involved with planning and
implementing ICT and Electronic Government programs, private sector
representatives, academics
BIO: Young Sik (YS) Kim is an Electronic Government Advisor at the
National Information Technology Center, Government of Nepal, on
assignment from the Korean International Cooperation Agency (KOICA).
He has jointed KOICA in 2005, after a 23 years career at IBM,
including four years at the IBM Global Services Unit in Tokyo, as
Systems Engineer, Project and Program Manager, Quality Assurance
Manager, and Project Executive. He managed large-scale system
development and integration projects particularly for Samsung, Hyundai
and Korean Air. Prior to joining IBM, he was a Navy Officer at the
Republic of Korea. Mr. Kim has a Telecommunication Engineering degree
from the Korea National Aviation University.
- 4
- Young Sik (YS) Kim, ICT Volunteer, Korean International
Cooperation Agency (KOICA), eGovernment Advisor, National Information Technology Center, Government of Nepal
10:00 - 11:30, Wednesday, 14 March 2007
Title: Developing e-Government, Korean Experience
Abstract: The Republic of Korea have achieved a remakable growth in
economy and social development within several past decades, beginning
as one of the poorest countries in the world. Information and
Communication Technology (ICT) and Electronic Government constitute
one of the focal areas to drive this development.
This seminar will present the history of economic development in the
Republic of Korea and in particular the development of ICT and
Electronic Government. The role of Korean Government to faciliate this
development and the roadmap to drive the future development of ICT and
Electronic Government will also be discussed. During the presentation,
critical success factors and lessons learned will be shared.
TARGET AUDIENCE: Government officials involved with planning and
implementing ICT and Electronic Government programs, private sector
representatives, academics
BIO: Young Sik (YS) Kim is an Electronic Government Advisor at the
National Information Technology Center, Government of Nepal, on
assignment from the Korean International Cooperation Agency (KOICA).
He has jointed KOICA in 2005, after a 23 years career at IBM,
including four years at the IBM Global Services Unit in Tokyo, as
Systems Engineer, Project and Program Manager, Quality Assurance
Manager, and Project Executive. He managed large-scale system
development and integration projects particularly for Samsung, Hyundai
and Korean Air. Prior to joining IBM, he was a Navy Officer at the
Republic of Korea. Mr. Kim has a Telecommunication Engineering degree
from the Korea National Aviation University.
- 3
- Abdel Hakim Hannousse, UNU-IIST fellow
15:00, Friday, 9 February 2007
Title: A Qualitative and a Quantitative Evaluation of Concern
Separation Approaches Based upon Design Patterns with AI and MAS
Application
Abstract: Conventional Object Oriented Model (OOM) has some limitations that
recent approaches known as Advanced Separation Of Concerns (ASOC) try
to eliminate. Nowadays, a large amount of literature devoted to three
ASOC approaches: Aspect Oriented Programming (AOP), Composition
Filters (CF) and Multi-dimensional Separation Of Concerns.
Unfortunately, the philosophy of each one is different and their
concepts used are not similar. Consequently, we need to compare them
in order to both unify and improve them. In order to contribute to
the assessment of ASOC approaches, we have undertaken a comparative
study whose originality dues to using design patterns as a benchmark
in that evaluation. Our idea consists of codifying patterns following
different ASOC approaches and assessing qualitatively and
quantitatively the obtained code. It describes how patterns are
implemented in each approach and compares the resulting code using
stringent software engineering metrics as assessment criteria. As a
first step, we have selected one pattern from each class of the GOF
classification which makes the comparison more significant and more
challenging. Integrating our process in the ordinary software
development process improves developed software quality.
- 2
- Prof. Xie Xiaoyao, Vice President, Guizhou Normal University
1500, Thursday, 8 February 2007
Title: Introduction to Two Recent Projects
Abstract: We introduce the two projects that we have just completed:
1. Red Maple Lake Long Span Bridge Health Monitoring System:
- Red Maple Long Span Cable-stayed Bridge is selected as an
experimental unit and will establish a demonstration project with
real-time online bridge health monitoring system
- High-precision vibration sensors will be used to measure the dynamic property
of cables and main beam
- Fiber Bragg grating sensors ( FBGS) will be used to measure the bridge strain
property
- GIS will be used to manage various information, such as map, bridge information,
the sensor position, etc.
- In order to monitor the bridge structures displacement,
high-precision GPS will be
used to measure all the designed points' 3D position periodically
- Large-scale Real-time Database will be used to manage the sensors
real-time data
- Remote communication is used to transmit the real-time data to monitor center
bridge safety evaluation expert system will be established for bridge safety and
traffic ability evaluation, maintenance solutions
2.
China Next Generation Internet In Guizhou Normal University
The Background of Deploying CNGI (China Next Generation Internet) in
GNU
The IPv6 and its development in GNU
Future Works
- 1
- G. P. Patil, Professor of Mathematical Statistics and Director of the Center for Statistical Ecology and Environmental Statistics in The Pennsylvania State University
10 - 11 January 2007
Title: Workshop on Digital Governance and Hotspot Geo-Informatics
Abstract: Geoinformatics for spatial and temporal hotspot detection
and prioritization is a critical need for the 21st Century. A declared
need is around for statistical geoinformatics and software
infrastructure for spatial and spatiotemporal hotspot detection,
prioritization, early warning, and sustainable management. A hotspot
can mean an unusual phenomenon, anomaly, aberration, outbreak,
elevated cluster, critical area. The declared need may be for
monitoring, etiology, early warning, or management. The responsible
factors may be natural, accidental, or intentional. The five year NSF
DGP project has been instrumental to conceptualize hotspot
geoinformatics partnership among several interested cross-disciplinary
scientists in academia, agencies, and private sector around the world.
Our efforts are driven by a wide variety of case studies of interest
to agencies, academia, and private sector involving critical societal
issues, such as public health, ecosystem health, ecohealth,
biodiversity and threats to biodiversity, emerging infectious disease,
water management and conservation, carbon sources and sinks,
persistent poverty, environmental justice, crop pathogens, invasive
species management, biosurveillance, biosecurity, disease
biogeoinformatics, social networks, sensor networks, hospital networks
and syndromic surveillance, video mining, early warning, tsunami
inundation, remote sensing, and disaster management. Also space-time
disease, poverty, pollution, object identification and tracking, early
detection, early warning, hotspot trajectories and trends with
examples of West Nile Virus, urban poverty patch dynamics, etc. The
project emphasis is on development of geoinformatic hotspot system and
its software. The system has two methodological components: hotspot
detection and prioritization.
The emphasis of the proposed two day workshop is also on
geoinformatics of hotspot detection and prioritization in a wide
variety of subject areas and critical issues confronting agencies,
academia, and industry. You are invited to participate in a manner
most productive for your purposes, whether in methods, tools, and
software, or in presentation of live case studies or in attendance in
a timely, informative, and insightful workshop. You have the benefit
of a veteran crossdisciplinary scientist as perceptive expositor,
workshop leader, and editor of resulting publications. And of course,
an opportunity to strengthen, advance, and accelerate your in-house
research and work plan involving geoinformatics and hotspot dynamics.
The proposed instructional part will provide up-to-date exposition
with live examples and illustrations. The proposed workshop part will
discuss case studies with emphasis on the methodology and software
available.
For general information on digital governance and hotspot
geoinformatics, please see http://www.stat.psu.edu//hotspots.