- Prof. Saleem Zoughbi, UNU-IIST Visitor from University of Bethlehem, Palestine
12:00 - 13:00, 16 January, 2004
Title: The Politics of Technology - A Case Study: The Middle East
Abstract:
1. Background of the Middle East crisis
2. Technology in the Middle East & relation to the West
3. Technology Parks, research projects and political games
4. Example: THE Internet in the Mediterranean
5. Example: Use of Software Technology economics to sustain political
ends
6. European efforts: The Information Society initiative
- Pham Hong Thai, UNU-IIST Fellow from Vietnam
16:00 - 17:00, 27 February, 2004
Title: On Checking Linear Duration Invariant for Timed Automata
Abstract:
In the report we show how to apply a minimization of timed
automata to check a class of formulas in Duration Calculus called
Linear Duration Invariant (LDI). As known, LDI has been checked
for many different systems by many different techniques, for
example by solving linear programming problems or exploring on
integral region graphs. However, almost known algorithms only
check for restricted semantics of LDI or for subclasses of timed
automata. In this report, we propose an algorithm to check LDI with its general semantics for timed automata.
In the algorithm, at first we use exploring technique on zone graph of timed automata to check LDI for
observation intervals which starting at the initial location of
timed automata. Next we prove LDI is discretisable formula and combining
above algorithm, we can check LDI for observation intervals which starting at the integral time points instead of real time points. Hence, LDI with general semantics is checked for timed automata.
- Prof. Matthew O ADIGUN, Department of Computer Science,
University of Zululand, Kwadlangezwa 3886 Republic of South Africa
15:00 - 16:00, 10 March, 2004
Title: Software Infrastructure for E-Commerce and E-Business- A Research Outlook
Abstract:
A research agenda is presented that is envisaged to contribute to three basic phases of e-Commerce, namely, Information search, Contracting and Delivery. The main goal is to generate advanced skills required to support the development of suitable software systems for the emerging mobile commerce era. The overall strategy is decomposed into a set research objectives given as follows. First, is to develop a critical mass of skills in e-Business process modelling. Second, is to create architectures for composing business processes from product line-based services. Third is to raise personnel with trusted services expertise to build reliability, security and safety into e-Services. And finally, to develop appropriate skills for building mobile commerce applications that meet the peculiar requirements of: minimal attention interfaces, dynamic environment, mobile device limitation and usability, and social concerns to name a few. The agenda includes a process of demonstrating our research results with relevant software products to the South African Tourism industry.
- Matthew ADIGUN, MO, Ph.D., University of Zululand, Department of Computer Science
15:00 - 16:00, 17 March, 2004
Title: Requirements for a Software Development Facility for a Research Centre: A Preliminary Investigation
Abstract:
An attempt has been made at putting together the requirements for a facility for developing enterprise-quality software systems. The focus of the investigation is to synthesize a core set of requirements; and to evaluate candidate software development environments against a set of criteria derived from both the requirements and documented relevant best practices. The competition is not simply between proprietary and open-source software. The result of the investigation depends on 'how much' the Centre will be willing to pay for getting the best tools into our development arsenal.
- Zhiming Liu, UNU-IIST Research Fellow
11:30, 18 March, 2004
Title: Formal Support to UML-Based Software Development
Abstract: - Li Xiaoshan
16:30, 18 March, 2004
Title: Prototype Generation from UML Requirement Analysis Models
Abstract: - Liu Jing, UNU-IIST Fellow
15:00, 29 March, 2004
Title: Linking UML Design Models and UML Requirement Models
Abstract: - Long Quan, UNU-IIST Fellow from Peking University
10:30, 30 March, 2004
Title: A Case Study: Formal Specification of CORBA
Abstract: - Prof. He Jifeng, UNU-IIST Senior Research Fellow
15:00, 30 & 31 March, 2004
Title: OOL and COOL - The Object-Oriented Language and Its Calculus for
Software Development
Abstract: - Elizabeth Vidal, UNU-IIST Fellow
16:30 - 17:30, 30 April, 2004
Title: How OCL may be used to enhance UML Class Diagrams
Abstract:
OCL is a language that can express information that is not explicitly present in UML diagrams used in OO models. OCL expressions are linked to diagrams' entities. This presentation aims to review these links, discuss briefly basic syntax and introduce the predefined types and their operations. Semantics assumed by the OMG for OCL will be shown. Presentation will be example based and will focus on class diagrams.
- Dr. Yifeng Chen, UNU-IIST Academic Visitor, Department of of
Computer Science, The University of Leicester, England
16:30 - 17:30, 7 May, 2004
Title: FLEXIBO Online Programming Environment
Abstract:
FLEXIBO is an executable specification language that supports prototype object-oriented programming in a decentralized multi-user development environment. FLEXIBO has a number of distinctive features:
Flexibility, as the main feature of FLEXIBO, is pursued throughout the design of the language. All language ingredients are values (i.e. data that can be manipulated by code), including primitive values, objects, classes, methods and program code (i.e. reflection). Flexible inheritance: values, classes, methods/specifications, Java classes, Java methods etc. have corresponding mirror classes in FLEXIBO. Mirror classes can be extended to subclasses by authorized users. Various language operators, including method invocation, type checking and object creation can be over-ridden in user-defined classes. Variables with different "colors": users may choose to write different kinds of variables in a program explicitly. This has solved some long-standing problems of reuse in OO inheritance mechanism.
FLEXIBO program code can be executed and tested online. In this sense, FLEXIBO is an interpreted programming language. Unimplemented specifications generate exceptions in execution. Since all types are values that can be manipulated by FLEXIBO programs, the FLEXIBO interpreter can thus be used as a translator from FLEXIBO to C++, Java or any other object-oriented languages. Users can design their FLEXIBO compiler to check types in runtime, which is, in fact, the compilation time of the translation. This feature is currently under development.
FLEXIBO supports a decentralized programming environment that allows specifications and different levels of trust between multiple users. Ownership control: a programmer may choose to protect any values including their code, data and even exceptions. This is particularly important if the contractor of a specification cannot completely trust the implementer. Resources control and pre-post specification (correctness control): contractors may set specifications with pre/post conditions together with resource restrictions. The violation of resource restriction by an implementer generates an exception, which cannot be caught by the implementer if the exception is ownership-protected. Redundant implementation: each specification may be implemented by one or several programs. A user may design their own specification and the corresponding scheduling algorithm by inheriting the mirror class of specifications, if multiple redundant implementations are available. Coding bugs naturally exist in any large scale software. The mission of FLEXIBO is not to eliminate those bugs. Instead, it provides the controlling mechanisms to limit the scope their effect.
FLEXIBO has full access to Java's classes, although the mirror class "JClass" is owned by the administrators and hence its access is strictly controlled according to the accessibility relation.
- Chris George, UNU-IIST Director
15:00, 10 May, 2004
Title: A little introduction to Perl
Abstract:
I am giving a brief introduction to Perl at 3pm today which you are welcome to join.
This is not a general introduction, but is intended merely to show how to solve one kind of problem (translating files from one format to another) in Perl.
It is not being given by an expert - I first started looking at Perl late last week, having failed to find anyone here to teach me!
You need to print and bring paper copies of the three files.
155501.rdf is a typical input file.
dublin_core.xml is the generated output.
mk_intech.pl is the Perl script.
- Chris George, UNU-IIST Director
17:00-18:00, 14 May, 2004
Title: How to give a good technical presentation
Abstract:
Some simple ideas can improve your presentation and report writing skills. These seminars show how to present to or write for your audience, so that they are more likely to remember what you presented or read and understand what you wrote.
- Chris George, UNU-IIST Director
16:00, 21 May, 2004
Title: How to write a technical paper
Abstract:
Giving presentations and writing papers are activities that academics, and others, have to do, but often find difficult. And it is more difficult in a foreign language. (Can you start a sentence with "and"?). This seminar aims to present some basic ideas that can help you improve your presentation and writing skills.
- Satyajit Acharya, UNU-IIST Fellow from Department of Computer and Informations Sciences University of Hyderabad, Hyderabad, INDIA
16:00, 28 May, 2004
Title: Specifying a Mobile Computing Application Environment Using RSL
Abstract:
Mobile computing shares many features with distributed computing, but it also extends the latter because of the need to deal with the mobility and occasional disconnection of both devices and applications.
In this report we give the RSL specifications to describe the behavior of applications in a mobile computing environment. Specifically, we give the specification for describing the migration, hoarding and cloning behavior of mobile applications.
Keywords: Mobile Computing; Graphical Notation; Mobicharts; Formal Specification; RAISE; Consistency Conditions; Testing.
- Dr. Yifeng Chen, UNU-IIST Visitor from Department of Computer Science
at the University of Leicester, England
16:30, 4 June, 2004
Title: Integrating Temporal Logics
Abstract:
In this talk, I will discuss the predicative semantics
of different temporal logics and the relationships between them.
We use a notation called generic composition to simplify
the manipulation of predicates. The modalities of possibility and
necessity become generic composition and its inverse of converse
respectively. The relationships between different temporal logics
are also characterised as such modalities. Formal reasoning is
carried out at the level of predicative semantics and supported by the higher-level laws of generic composition and its inverse.
Various temporal domains are unified under a notion called
resource cumulation. Temporal logics based on these temporal
domains can be readily defined, and their axioms identified. The
formalism provides a framework in which human experience about system development can be formalised as refinement laws. The
approach is demonstrated in the transformation from Duration
Calculus to Temporal Logic of Actions. A number of common design
patterns are studied. The refinement laws identified are then
applied to the case study of water pump controlling.
- Dr. Yifeng Chen, UNU-IIST Visitor from Department of Computer Science
at the University of Leicester, England
15:00-17:30, 8-10 & 15-16 June, 2004
Title: Formal Software Specification
Abstract:
This course demonstrates the use of mathematics to formally
specify the requirements of a computer system, and then to
develop correct code meeting those requirements.
One of the most common causes of errors in computer systems is
that the requirements are incorrectly understood. The purpose of
a formal specification is to set down concisely and unambiguously
what is required. A good specification concentrates on
specifying what is required, not how it will be
achieved. To this end, states are specified abstractly (for
example, using sets and mappings rather than concrete datatypes
such as linked lists or arrays), and specifications are written
for the required operations, describing how the state should
change.
The process of going from a specification to an implementation is
known as refinement. There are two forms of refinement:
data refinement and program refinement. Data refinement is
concerned with the replacement of the high-level abstract
datatypes (e.g. sets and mappings) by the implementable
data-types found in languages such as Pascal (e.g. linked lists
and arrays). Program refinement is the other part of software
development: that of turning specifications into algorithms.
- Dr. Joseph S P Fong, Department of Computer Science at City University of Hong Kong
11:30, 14 June, 2004
Title: Transformation of Relational Database to XML
Abstract: - Kim Pyong Sam, UNU-IIST Fellow
15:30, 17 June, 2004
Title: An UTP Approach to Semantics for Component-Based Real-Time Systems
Abstract:
This report defines some compound operations over timed designs (like sequential, conditional and so on) by using UTP approach, presents some algebraic laws from them and then verifies the soundness of these operations by using the operational semantics. Also, it represents some concepts and finds some properties concerning the component system. In order to support to specify and verify the temporal and real-time requirements, it formalises the ITL semantics of compound timed designs and finds their properties.
- Kim Yong Chun, UNU-IIST Fellow
15:30, 18 June, 2004
Title: Verifying Real-time Systems Using Standard Model Checking Tools
Abstract:
In this talk, we present a way to verify real-time systems using untimed model checking tools through a verification case study with standard SPIN.
We introduce a class of DC whose formulas correspond to regular expressions over the set of special symbols, each of which is a state occurrence for one time unit or for less than one time unit. The length of string will reflect a time constraints. These regular expressions can be translated easily to untimed automata or a SPIN model. In this way, we can verify real-time systems in the usual way for verifying untimed system with standard SPIN.
- Dr. Mike Reed, Oxford University, UK
15:00, 24 June, 2004
Title: Order, Topology and Induction Recursion in CSP
Abstract: - Elizabeth Vidal Duarte, UNU-IIST Fellow
15:30, 25 June, 2004
Title: Computer Science Curriculum Design for Developing Countries: a Peruvian Case Study
Abstract:
The task of establishing a new CS career in a university in a developing country is a challenging one. Designing an appropriate curriculum is a crucial part of this challenge. The objective of this seminar is to present how to design and improve a curriculum in CS for a developing country such as Peru. The process is based on the Computing Curricula 2001 project of IEEE and ACM which provides guidelines for undergraduate programs in computing. The seminar presents the process and results of improving the current Informatics Engineering curriculum at the Catholic San Pablo University in Arequipa, Peru.
- Chris George, UNU-IIST Director
11:00, 2 July, 2004
Title: Proving safety of authentication protocols: a minimal approach
Abstract:
Internet security depends on encryption but also on authentication of the other party, so you know for example that you are not sending your credit card number to amazon.con.
This seminar briefly describes how authentication protocols work, and also describes in detail a formalization and proof of the Needham-Schroeder protocol.
- Prof. Saleem Zoughbi, UNU-IIST Visitor from University of Bethlehem, Palestine
15:30, 9 July, 2004
Title: Modelling an automated system, that manages the mapping and splitting of parallel databases for better efficiency of access of distributed systems
Abstract:
The problem of splitting this large database into clusters and shipping them
from one place to another across the nodes of the network would yield to a
very reasonably and agreeably performance for large distributed DB systems.
Selecting the splitting method and implementing it according to a
distributive plan could be programmed to run automatically.
This talk will focus on the idea of using Adaptive digital filter technique
in order to monitor, decide and implement parallelism in distributed heavy
data base applications.
- Ho-Fung Leung, Associate Professor from Department of Computer
Science and Engineering at The Chinese University of Hong Kong, Shatin, N.T., Hong Kong SAR, P.R. China
15:00, 13 July, 2004
Title: Honesty, Trust, and Rational Communication in Multiagent Semi-competitive Environments
Abstract:
This talk introduces rational communication among agents in multi-agent semi-competitive environments. In such environments, agents have both incentives to be honest and to be dishonest. Therefore, agents need to decide whether or not to trust other agents. This talk differentiates the concepts of reputation, impression and trust; proposes to include the agent's attitude towards risk in deriving the trustworthiness from the impression of another agent; and proposes to integrate an agent's impression towards the message sender, the agent¡¦s attitude towards risk, and the utility brought by believing the message in making decisions on whether to believe a message and change its action based on the message. These mimic the model in human interactions.
- Javier Larrosa, Associate Professor from Departament de
Llenguatges i Sistemes Informatics at Universitat Politecnica de
Catalunya (UPC), Barcelona, Spain
16:30, 13 July, 2004
Title: Algorithms for weighted constraint satisfaction problems
Abstract:
Constraint Satisfaction Problems (CSP) involve a finite set of variables and a set of constraints among them. A solution is an assignment to the variables that satisfies all the constraints. The CSP framework allows to express in a natural way many combinatorial problems. Besides, efficient solving techniques have been developed during the last decades. Recently, the CSP framework has been augmented to acomodate optimization problem. One of these extensions is the Weighted CSP framework, which can be used to express combinatorial optimization problems where the objective function is a sum of arbitrary cost functions. Some application examples can be found in Economics (f.eg. combinatorial auctions), Bioinformatics (f. eg. sequence alignment), resource allocation (f.eg. frequency allocation problems), etc. In this talk I will motivate the framework and review the two main solving techniques. First I will discuss systematic search, a complete solving method. Next I will define some forms of local consistency. Although local consistency is incomplete and cannot be used as a stand alone method, we will see that it can be naturally combined with systematic search leading to state-of-the-art algorithms.
- Prof. Saleem Zoughbi, UNU-IIST Visitor from University of Bethlehem, Palestine
15:00, 3 August, 2004
Title: Reconciling the Should-be and the Can-be in Undergraduate Curricula: Lessons from Bethlehem University, Palestine
Abstract:
The issue of computer science curricula on the undergraduate level has been one of the main issues of higher education strategic planning and development. This is not only true for well-developed countries, but as the information revolution has already swept this planet with all its countries in all categories, so called "developing countries" have witnessed an ever-increasing will to adopt such curricula. The issue studied in this report is whether curricula-transfer (in the sense of "technology transfer") would be best suited or to reinvent the wheel again and start developing a specific curriculum that fits each country accordingly. Naturally a balance has to exist somehow since neither option is feasible. This talk does not intend to survey existing curricula reports or existing case studies of established curricula in universities in other countries. It studies such balance, and matches this balance to a developing country like Palestine within the case of Bethlehem University curriculum development for an undergraduate degree program in computers and information systems.
- Prof. He Jifeng, UNU-IIST Senior Research Fellow
15:00, 6 August, 2004
Title: How to integrate various tools based on different semantic
frameworks
Abstract: - Chris George, UNU-IIST Director
10:00-13:00, 6-10 September, 2004
Title: Formal software specification and development using RAISE
Abstract:
RAISE - Rigorous Approach to Industrial Software Engineering - was first developed in European collaborative projects during 1985-94. The RAISE Specification Language (RSL) is wide spectrum, supporting descriptions ranging in style between abstract and concrete, applicative and imperative, sequential and concurrent. RSL is also modular, supporting the writing of large descriptions.
RAISE includes a method for software development, and also a set of free, open-source, portable tools. Tool supported activities include generation of specifications from UML class diagrams, validation and verification of specifications, refinement, prototyping, execution of test cases, mutation testing, test coverage analysis, generation of documents, and generation of program code in C++ by translation.
The course will introduce the language and method, and also include practical work with the tools.
- Xinbei Tang, Computing Laboratory, University of Kent, UK
15:00, 13 September, 2004
Title: Travelling Processes
Abstract:
This talk describes a refinement-based development method for mobile processes. Process mobility is interpreted as the assignment or communication of higher-order variables, whose values are process constants or parameterised processes, in which target variables update their values and source variables lose their values. The mathematical basis for the work is Hoare and He's Unifying Theories of Programming (UTP). In this talk, we present a set of algebraic laws to be used for the development of mobile systems. The correctness of these laws is ensured by the UTP semantics of mobile processes. We illustrate our theory through a simple example that can be implemented in both a centralised and a distributed way, and we show how the centralised system may be step-wisely developed into the distributed one using our proposed laws.
- Dang Van Hung, UNU-IIST Research Fellow
10:00-13:00, 14-16 September, 2004
Title: Introduction to Model Checking Techniques
Abstract:
This course gives an introduction to model-checking, a technique for automatic verification of software and reactive, real-time systems. Model checking was invented long time ago, and has been used successfully in many industrial projects. Many researches in this topic are still in progress. This course will give the basic elements required for understanding model checking, and the basic skills for using model checking tools. It also provides the basic knowledge for the researchers to start doing research in this topic.
(Please visit http://www.iist.unu.edu/home/Unuiist/newrh/II/2/1/7/page.html
for more details on the course)
- Bhim P. Upadhyaya, UNU-IIST Fellow from Nepal
15:00, 17 September, 2004
Title: A formal model for JavaBeans
Abstract:
Component based software development focuses on building software systems by assembling existing software components. This makes the systems more maintainable, reduces devlopment time and minimizes development as well as maintenance costs. The Java programming language supports component based software development through JavaBeans. Specifying JavaBeans in a natural language is ambigious to the software systems developers. The use of a formal technique helps to express JavaBeans and consequently JavaBeans-based software systems precisely. In this seminar, we present a formal model of JavaBeans, whereby a system can be divided into a number of interconnected JavaBeans. We adopt the notion of refinement to formalize the replaceability of JavaBeans.
- Carlo Corrales Delgado, UNU-IIST Fellow and Lecturer UNSA - UCSM. Arequipa, Peru
16:30, 17 September, 2004
Title: Test Purpose Generation by Specification Mutation in Distributed Systems
Abstract:
Mutation Testing is a fault-injection technique which can assess how
thoroughly a set of test cases exercises an implementation. We modify
the approach in two ways: First, it is applied on the specification
level, second, test cases are generated rather than assessed. More
precisely, we generate a test purpose which is an abstract description
of a test goal. Then, using the TGV test case generator, the actual
test cases can be generated from a test purpose. In this talk, we
describe our fault-based testing approach as well as the use of the
CADP tools to automate it. In addition, we briefly present a short
case study applying the method to test a HTTP web server.
- W. Eric Wong, Department of Computer Science, University of Texas at Dallas
15:00, 4 October, 2004
Title: Testing and Diagnosis of Software Design Specifications
Abstract:
Statistical data show that early fault detection in the software
development process can cut cost significantly. Additionally,
with improved technology for automatic code generation from
architectural design specifications, it becomes even more important
to have a highly reliable system design from the beginning.
To ensure this, the quality of the system must be predicted and
improved as early as possible. This talk will focus on how to
extend source code-based techniques to the software design
specification level to allow more efficient specification
validation and maintenance. Also discussed will be a novel
approach for constructing a small set of effective test sequences
from a design model to satisfy certain structural coverage criteria.
These tests can be used not only for conformance testing with a
focus on the consistency between the specification and the
implementation but also for the validation of the design
specifications themselves.
Bio: W. Eric Wong received his B.S. in Computer Science from Eastern
Michigan University, and his M.S. and Ph.D. in Computer Science
from Purdue University. In 1997, Dr. Wong received the Quality
Assurance Special Achievement Recognition from Johnson Space Center,
NASA. Currently, he is an associate professor in Computer Science
at the University of Texas at Dallas. Before joining UTD in 2002,
he was with Telcordia Technologies (formerly Bellcore) as a senior
research scientist and a project manager in charge of the initiative
for Dependable Telecom Software Development. Dr. Wong's research
focus is on the development of techniques to help practitioners
produce high quality software at a low cost. In particular, he is
doing research in the areas of software testing, reliability,
metrics, and QoS at the application, as well as architectural
design, level. He served as general chair for ICCCN 2003 and
program chair for Mutation 2000, ICCCN 2002, COMPSAC 2004,
SEKE 2005 and ISSRE 2005. He is a senior member of IEEE.
More details on Dr. Wong's research, grants and publications are
available at his home page:
www.utdallas.edu/~ewong.
- Zhiming Liu, UNU-IIST Research Fellow
15:00-17:00, 8 October, 2004
Title: UML: Promises, Problems and Solutions
Abstract:
Being called a "Unified" modelling language, UML promises quite a lot. However, coming along with the promises, there are important problems need to be solved, problems regarding the letter "U" in particular.
This talk discusses the promises and the problems in the use of UML in software
development.
We will also look at the research directions in formal support of UML. We will then discuss the the idea of using a formal component-based and object-oriented specification language (CBOOL) to formalize and combine UML models. With the formalization, we develop a set of refinement laws of UML models to capture the essential nature, principles and patterns of object-oriented design. With the the incremental and iterative features of object-orientation and the Rational Unified Process (RUP), our method supports precise and consistent UML model transformation.
- Joseph Fong, Associate Professor in the Computer Science
Department, City University of Hong Kong
11:00, 11 October, 2004
Title: Reverse engineer XML database into a conceptual model
of Document Type Definition Graph
Abstract:
To design an XML database is an issue, but to implement an
XML database design correctly is another issue. It is necessary to
verify the data semantics of an XML document according to users data
requirements. However, there is no standard XML conceptual model
yet. Furthermore, one has to navigate through an XML document to
access the data occurrence paths of its elements. In particular, its
IDREF may refer to a wrong ID or nowhere. Thus, we need an XML
conceptual model to realize the current state of data semantics of an
XML database. Our objective is to capture data semantics of
cardinality, weak entity, participation, isa, generalization,
aggregation, categorization and n-ary relationship in terms of
elements, sub-elements, group elements, component elements, occurrence
indicator, ID and IDREF in an XML conceptual model. This seminar aims
to provide a solution by reverse engineering an XML document into a
Document Type Definition Graph. The Document Type Definition Graph
validates the IDREF values by browsing through the XML document, and
presents a validated XML schema in a diagram. The result is a Document
Type Definition Graph, which can act as an XML conceptual model to
help users to recover the data semantics of an XML document. The
Document Type Definition Graph transforms the constraints of an XML
schema in a topological structure of hierarchy nodes representing all
elements within an XML schema. It can also be used to confirm the
constraints according to the user requirements. The derived XML
conceptual model helps a better understanding of an XML document. The
success of this research project can be toward the establishment of a
standard XML conceptual schema.
Speaker: Joseph Fong is an Associate Professor in the Computer Science
Department at City University of Hong Kong. He is a former chair of
the Hong Kong Computer Society Database Special Interest Group, and
the founder chair of Sybase Hong Kong User Group, Hong Kong Web
Society, and an annual International Conference on Web-based learning.
- Dr. Vassilios Persiteras, UNU-IIST Visitor from Greek National Centre for Public Administration and Local Government
16:30-17:30, 4 November, 2004
Title: The Governance Enterprise Architecture (GEA)
Abstract:
Public administrations all over the world promote ambitious
and costly e-government programmes. The required domain analysis for
these projects is usually conducted on a local and ad hoc basis, due
to a lack of commonly agreed content standards, definitions and
vocabularies, not only at the global level among administrative
systems worldwide, but even within each country. To address this
shortage, we propose the Governance Enterprise Architecture (GEA) as a
broad research conceptual modeling effort, which aims at developing a
series of generic top-level models for the overall governance system.
These models could serve among others as (a) a common language for
communication amongst researchers and practitioners from different
disciplines (e.g. IT, public policy), (b) an upper ontology for public
administration, and (c) a part of an e-government ERP kernel that
could be easily parametrized and configured for a variety of different
services offered by public administration at its different levels and
in different countries. Moreover, the experience of using these models
in order to implement public administration services upon a Semantic
Web Service technological infrastructure will be briefly presented.
Bio: Dr. Vassilior Peristeras works for the Greek National Centre for
Public Administration and Local Government. He heads the Centre's
branch in Thessaloniki. Dr. Peristeras has studied Political Science,
has two Masters degrees in Public Administration and Information
Systems and a PhD in Information Systems for Public Administration.
He has worked as a researcher at various EU-funded R&D projects in the
field of e-government, and has been at the UN as an IT consultant. Dr.
Peristeras has an extensive experience on e-government national
strategy development, in particular he participated in various stages
in the Greek governmental programme for Information Society.
- Zhiming Liu, UNU-IIST Research Fellow
15:00-18:00, 15-17 November, 2004
Title: Real-Time Systems: Specification, Verification, Refinement and Schedulability
Abstract:
Fault-tolerance and timing have often been considered to be implementation
issues of a program,
quite distinct from the functional safety and
liveness properties. Recent work has shown how these non-functional and
functional properties can be verified in a similar way.
However, the more practical question of determining whether a real-time
program will meet its deadlines, i.e., showing that there is a feasible
schedule, is usually done using scheduling theory, quite separately from
the verification of other properties of the program. This makes it hard to
use the results of scheduling analysis in the design, or redesign, of
fault-tolerant and real-time programs.
This course discusses how fault-tolerance, timing, and schedulability can
be specified and verified using a single notation and model. This
allows a unified view to be taken of the functional and nonfunctional
properties of programs and a simple transformational method to be used
to combine these properties. It also permits results from scheduling
theory to be interpreted and used within a formal proof framework.
The notation and model are illustrated using a simple example.
- Prof. Dines Bjorner, founder director of UNU-IIST, Professor of the University of Denmark
10:00 - 12:30, Tuesday 30 November - Friday 3 December
Title: Issues of Domain and Requirements Engineering and of Software Architecture
Abstract: The TripTych Approach to Software Development, Domain Facets, and Software Architecture + Components Design
