II/5/14 Seminars and Colloquia 2008

 

20

Alejandro Sanchez
10:00, Friday 27, June
Title: Semantic Interoperability for Electronic Government
Abstract: Information systems in different public agencies frequently need to exchange information to support seamless and one-stop services delivered to government customers. For such exchange to be successful the systems must be organizationally, semantically and technically interoperable. Out of these conditions, semantic interoperability is posing the greatest technical challenge.

In this seminar we discuss the problem of semantic interoperability and specify concrete requirements for any semantic interoperability solution. Subsequently, we propose a middleware-based solution - Semantic Interoperability Middleware (SIM) to address some of these requirements using three basic services: semantic validation, semantic mediation and semantic discovery. During the seminar, we present the architecture and design models of the SIM, along with their underlying ontologies, and demonstrate three e-Government applications that rely on SIM to resolve concrete semantic interoperability cases.

 

19

Mohamed Shareef, Assistant Director General, National Centre for Information Technology, Republic of Maldives
12:15, Friday, 20 June
Title: Assessing e-Government Readiness in the Maldives
Abstract: There is an increasing evidence that Electronic Governance can effectively support major transformation objectives of the countries like Maldives that undergo multi-faceted transition in the areas of democratic governance, economic development and knowledge society. However, an effective Electronic Governance program requires a coherent set of policies and strategies to guide the development of the necessary regulatory frameworks, organizational and technical infrastructures, and information systems. One of the challenges that Maldives faces in developing its Electronic Governance strategy is the absence of detailed information on Electronic Government readiness of its various ministries, department, agencies, and islands. Apart from the complexity and high resource requirements of national readiness assessment exercises, there is a general lack of suitable e-readiness assessment frameworks applicable to the public sector. One of such frameworks is the e-Macao e-Readiness Assessment Framework. The aim of this work is to tailor and apply this framework to satisfy information requirements for Electronic Governance strategic planning in Maldives.

The seminar first provides some background on Electronic Governance development in the Maldives, from ICT policy framework to concrete initiatives. Next, it examines the major challenges to Electronic Governance development in the country, focusing on the lack of comprehensive e-readiness data to support effective planning. After examining a number of publicly available e-readiness assessment frameworks with respect to the Maldives assessment requirements, it proposes how the e-Macao e-Readiness Framework could be extended to obtain a concrete e-readiness assessment instrument for Maldives.

Biography:

Mohamed Shareef is the Assistant Director General of the National Centre for Information Technology, Government of Maldives (NCIT), and the head of the e-Government Services division of NCIT; NCIT is the organization responsible for developing Electronic Government in the country. Mohamed Shareef has been actively involved in the development of Electronic Government in Maldives since 2003, being responsible for managing the development of the Government Network of Maldives, e-Government Service Platform and a number of e-Government applications. He holds a Master of Engineering degree from the University of Birmingham, UK.

 

18

Radha Chauhan, Principal Consultant, National eGovernance Plan, Department of Information Technology, Government of India
11:30, Friday, 20 June
Title: Sustaining Electronic Governance - Critical Factors and a Policy Intervention Model
Abstract: One of the foremost challenges for the development of Electronic Governance is how to ensure that the whole effort, and the public value generated through it, can be sustained. This is particularly important, and challenging, in the context of a developing nation. This seminar presents the results of a study that aims to identify critical factors that impact sustainability of Electronic Governance initiatives. Drawing on the experience of several countries that lead the development in this area and the speaker's own experience working for the Government of India, the seminar goes on to present a model for policy interventions that aims to address these critical factors, and validates the model through the case of the National eGovernance Plan of India.

Biography:

Radha Chauhan acquired almost two decades of government experience working in various capacities as Indian Administrative Service officer. The major part of her experience has been in implementing government policies and programmes in a challenging State of Uttar Pradesh, well known for its complex societal landscape and heightened sensitivity to politics. Presently, she is a Principal Consultant in the Programme Management Unit of the National eGovernance Plan, under the Department of Information Technology, Government of India, part of the group that steers and coordinates national initiatives in this area at the policy level. Radha Chauhan holds a degree from the Faculty of Law, Delhi University.

 

17

Pieter Mosterman, The MathWorks, Inc., Natick, USA
14:00, Monday, 30 June
Title: Model-Based Design - An overview and research
Abstract: Model-Based Design is increasingly adopted in industry. This has resulted in a need for supporting an enterprise-wide use of models. As such, it has to be dealt with computational models that are designed in many different formalisms, that have very different computational semantics, and that capture the same parts at very different levels of detail or in different stages of design. A Computer Automated Multiparadigm Modeling (CAMPaM) framework is outlined that can be used to support and facilitate Model-Based Design. In addition to recent CAMPaM research, hybrid dynamic systems are presented as a mathematical framework for execution. Paradigmatic and pathological behaviors are illustrated by means of a multiple phase space transition ontology.

Biography:

Pieter J. Mosterman is a senior research scientist at The MathWorks, Inc. in Natick, MA. Before, he was a research associate at the German Aerospace Center (DLR) in Oberpfaffenhofen. He has a Ph.D. degree in Electrical and Computer Engineering from Vanderbilt University in Nashville, TN, and a M.Sc. degree in Electrical Engineering from the University of Twente, Netherlands. His primary research interests are in Computer Automated Multiparadigm Modeling (CAMPAM). He designed the Electronics Laboratory Simulator, nominated for The Computerworld Smithsonian Award by Microsoft Corporation. He was awared the IMechE Donald Julius Groen Prize for a paper on HYBRSIM, a hybrid bond graph modeling and simulation environment. Dr. Mosterman is currently Editor-in-Chief of SIMULATION: Transactions of The Society for Modeling and Simulation International for the Methodology section, and Associate Editor of IEEE Transactions on Control Systems Technology and of Applied Intelligence. He was Guest Editor of special issues of SIMULATION, ACM Transactions on Modeling and Computer Simulation and IEEE Transactions on Control Systems Technology on the topic of CAMPAM

 

16

Michael Weber, University of Twente, The Netherlands
11:00, Thursday, 15 May
Title: NIPS: Towards Reusable Components in Model Checking Tools
Abstract: The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages.

To evaluate the benefits of the proposed approach, several tools have been built around the VM implementation we developed, among them a model checker for Embedded Systems software.

Biography:

Michael Weber is working as VeriGEM Post-Doc at University of Twente (NL) in the Formal Methods and Tools group. He obtained his doctoral degree from RWTH Aachen University (D) on parallel and distributed verification algorithms. His interests are scaling up model-checking algorithms to modern multi-core computers and GRIDs, as well as I/O-efficient settings. His contributions include development of model-checking tools for C code written for various micro-controllers. He is also interested in the semantics of modelling languages, in particular to provide formal semantics for the input language of the SPIN model checker, PROMELA, and bridging the gap between action-based process algebras and state-based formalisms. He is in close collaboration with ParaDiSe Labs at MUNI Brno (Czech Republic) and their DiVinE model-checking toolkit, as well as INRIA Rhône-Alpes in the Dutch-French SENVA collaboration

 

15

Dang Van Hung, Institute of Information Technology, Vietnamese Academy of Science and Technology
15:00, Wednesday, 30 April
Title: Reasoning about QoS Contracts in the Probabilistic Duration Calculus
Abstract: The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus.

 

14

Abigail Vargas, UNU-IIST
15:00, Friday, 25 April
Title: Formalising the translation from RSL to CSP
Abstract: Our aim is to exploit the FDR model checker for descriptions of concurrent systems written in the RAISE Specification Language (RSL). To do this we define a translation from RSL to CSPM, show that the translation is a bisimulation, and then that various properties are preserved by bisimulation. This allows us to infer properties of the RSL description from the results of running FDR.

 

13

Professor Zuohua Ding, Zhejiang Sci-Tech University
15:00, Wednesday, 23 April
Title: Detecting Program Deadlock With Ordinary Differential Equations
Abstract: The state explosion problem has bothered us for decades in the static analysis of concurrent programs for deadlock detection. We propose a new method that can be easily used to detect program deadlocks in a practical way. Most importantly, it can completely avoid the state-explosion problem. A concurrent program can be described by a group of ordinary differential equations, where each equation describes the program state change. Therefore, instead of counting states as in discrete event systems to analyze the program, we can analyze the solutions of the equations. A program state can be measured by a number between 0 and 1. This measure indicates the extent to which the state can be reached when the program executes. At any time instant, a program attributes a measure to each state. We find that a program deadlocks if and only if every state measure of the program approaches either 1 or 0. Two types of deadlock models are considered in this talk: the communication (OR) model and the resource sharing (AND) model. All the equations can be solved by Matlab and by inspecting the solution curves we can tell if a program deadlocks.

 

12

Lizeth Tapia, UNU-IIST
16:30, Friday, 11 April
Title: Model checking concurrent RSL with CSPM and FDR2
Abstract: RAISE Specification Language (RSL) is a formal specification language that allows a wide range of specification styles (of datatypes, functions and processes). On the other hand FDR2 is a model checker for establishing properties of models expressed in CSPM; CSPM is the combination of functional programming language with the CSP process-algebra, CSPM is focused in process modelling and parallel systems.

The aim of our project is to apply model checking techniques over formal specifications expresed in RSL using FRD2; for which we have developed a first version of a translator between RSL and CSPM. In this talk we give an overview of the principal semantic and syntactic differences of this two languages and show the strategy used to find the respective equivalences in order to make the translation possible, then we briefly talk about the development of the translation tool and finally we show the use of the translator tool with some typical concurrent examples.

 

11

Yifeng Chen, Department of Computer Science, University of Durham
15:00, Friday, 11 April 2008
Title: Verifiers Are Programs
Abstract: This talks discusses the relation between execution and verification. A simple imperative language with execution and verification commands is introduced. A machine only executes execution commands of a program, while the compiler only performs the verification commands. Common commands in other languages can be defined as a combination of execution and verification commands. Design of verifiers then becomes program design using verification commands. It is shown that type checking, abstract interpretation, modeling checking and Hoare Logic are all special verification programs, so are many of their combinations.

Biography:

Before Joining Durham, He was a Lecturer at Department of Computer Science, University of Leicester between 2000 and 2004 , received a DPhil in Computing from Balliol College, University of Oxford in 2001, worked as an RA at Peking University in 1997 and received a BSc in Computer Science from Peking University in 1996. His main interests lie in imperative, parallel and object-oriented programming languages, including design, translation, static analysis, semantics and specifications.

 

10

WU Nan, Nanjing University
11:00, Friday, 11 April 2008
Title: Scalable Architecture of a Universal Quantum Computer with Fault Tolerance and High Performance
Abstract: Quantum computation is a field of science and technology, combining and drawing on the disciplines of physical science, mathematics, computer science, and engineering. Indeed, scientists predict that within the next 30 to 50 years there will be quantum computers. The architecture of a quantum computer is therefore worthy of study. Today, most of the physically implemented quantum devices can deal with only some specific problems or algorithms. People have been trying to build a universal quantum computer, which would be able to solve all kinds of problems on a single architecture.

In recent years, quantum algorithms, quantum computational models and physical quantum computers have been studied. The results of these studies provide the necessary theoretical and experimental basis to design the "next generation" scalable universal quantum computer with new features such as fault tolerance, high performance, and high-fidelity teleportation, etc. These features can also provide quantum operating system, quantum programming languages and their compilers, the basis for implementation and the platforms for execution.

This talk presents a scalable architecture of a universal quantum computer with fault tolerance and high performance.

Biography:

WU Nan received the B.Sc. degree in Computer Science from Nanjing University in 2004. He is now a PhD candidate in the Department of Computer Science and Technology at Nanjing University. His research interests mainly include quantum information processing, quantum-computer architecture and quantum programming languages.

 

9

Matthias Weber, CARMEQ
11:00, Thursday, 20 March 2008
Title: Developing Embedded Automotive Systems
Abstract: This seminar will present an overview of the results of a European-Union-funded project that involved car manufacturers and suppliers, and universities. The main result of the project has been an architectural-design language for automotive systems. The language is broad enough to include concepts for managing market lines, a topic that is chosen as a focus for this talk. A feature will be reflections on the place of Formal Methods in realistic Software Engineering.

Biography:

Matthias Weber was an undergraduate in Computer Science at the University of Karlsruhe and obtained his Habilitation from the Technical University of Berlin. After spending a decade working in Formal Methods at the TUBerlin, he has spent a further decade working in the German automotive industry - originally for Daimler and more recently for CARMEQ. He and Viktor Friesen, a colleague with a similar background but who works for Daimler, are visiting Jeff Sanders (whom they have known for two decades) for a fortnight.

 

8

Zhang Yu, Macao University of Science and Technology
11:00, Friday, 29 February 2008
Title: Cryptographic logical relations -- Yet another framework for verifying security protocols
Abstract: Formal verification of cryptographic protocols has been a very active research field for over a decade and it has been well accepted that many security properties, e.g., the secrecy property, can be formalized using the notion of contextual equivalence (a.k.a. observational equivalence) of programs. In typed lambda-calculi, contextual equivalence can usually be proved through a technique called logical relations. However, applying logical relations in the setting of protocol verification is not straightforward. We have in particular concentrated on the dynamic key (nonce) generation, which plays an important role in protocols but is unfortunately detoured by informal conventions in most models. Our work is based on the general model of deriving logical relations for monadic types (by Goubault-Larrecq et al.) and we propose a new categorical model Set^{PI->} based on Stark's name creation monad. We argue that this should be the right category for defining cryptographic logical relations. Interestingly, this research also leads us to an exploration of what should be the correct definition of contextual equivalence in the framework. We finally arrive at a definition also based on the new category, where represent faithfully the capability of adversaries, and we prove that our cryptographic logical relations are sound w.r.t. the contextual equivalence. The approach is applied to proving the correctness of the Needham-Schroeder-Lowe protocol in the Dolev-Yao model.

As the work includes many technical details, I will make the effort to give a general introduction to protocol verification. In addition to introducing the formal models, based on the framework mentioned above of course, we shall also talk about some topics at the frontier of the field, especially the more refined computational model where more realistic crypto-systems are taken into account. We will discuss on the possibility of extending our framework to fit in the computational model.

Biography:

ZHANG Yu is an assistant professor in Macao University of Science and Technology. He got his PhD from École Normale Supérieure de Cachan in France in 2005. Before moving to Macao he had also been working in CEA (the French Commissariat of Atomic Energy) and INRIA Sophia-Antipolis. His research interest addresses essentially on the formal verification of security protocols, using in particular logical methods from type theory, semantics of programming languages, etc. At MUST he is teaching two courses for the moment: Computer Architecture and Analysis of Security Protocols.

 

7

Fabrizio Luccio, University of Pisa, Italy
11:00, Friday, 22 February 2008
Title: A Boolean approach to transaction mining for discovering frequent itemsets (work in progress
Abstract: Managing frequent itemsets is a fundamental problem in managing large databases of customer transactions. To ease the mining process, closed itemsets have been defined as candidate for expressing the problem without loss of information. However, the number of such itemsets may be exponential in the size of the input. In this work we are trying to apply Boolean algebra methods for circuit design to describe the itemset problem in a much more compact way than the one used in current database technology. New Boolean techniques are being developed for the present problem that might be useful also for special circuit synthesis. Suggestions on this work are highly welcome.

Biography:

Link: Biography

 

6

Padmanabhan Krishnan, Bond University, Australia
11:00, Monday, 18 February 2008
Title: Secure Document Circulation
Abstract: Interoperable e-business applications are essential for increasing efficiency in the digital economy. In this talk we present an architecture for secure document circulation designed for securing information flow for interorganisational workflows. We also describe the key aspects of a prototype implementation.

Slide available: slide

 

5

Thomas Anung Basuki, UNU-IIST
11:00, Friday, 15 February 2008
Title: Model-checking Biological Systems using Calculi of Looping Sequences
Abstract: Recent advances in cell biology have made biologists realise that a cell is a very complex system. Computer modelling can help biologists to understand more about cell activity, behaviour and interaction with the environment. Formal methods developed for concurrent systems have been applied to model and reason about cells. All formalisms that have been proposed are only partly capable to model biological systems. Calculi of Looping Sequences are a class of formalisms that can model both the structure of cells and the activities occuring inside them. Stochastic CLS, a formalism belonging to this class, supports stochastic modelling and simulation of biological systems. However, analysing a system only through simulation has some limitations. Not all possible behaviours of the system can be covered by traditional simulation. These limitations can be overcome by using model-checking, a verification technique that performs exhaustive simulation of the system model. In this seminar we propose an approach to model-check Calculi of Looping Sequences models.

Slide available: slide

 

4

Chris George, UNU-IIST
11:00, Friday, 1 February 2008
Title: An algorithmic problem: grids to shapes
Abstract: This is an informal, interactive seminar in which we look at the problem of efficiently converting large grids (arrays of values) into polygonal shapes. Participants are invited to consider the problem beforehand and be ready to briefly explain their intended approach.

Slide available: Grids to shapes

 

3

Chris George, UNU-IIST
11:00, Friday, 25 January 2008
Title: The WaterBase Project
Abstract: WaterBase is a UNU project, joint between UNU-IIST and UNU_INWEH, to promote Integrated Water Resources Management (IWRM) in developing countries. It aims to promote IWRM by building a network of users and developers of a suite of modelling and decision support tools, together with other on-line resources. The first such tool, which supports river basin modelling, has just been released. See http://www.waterbase.org.

Slide available: WaterBase

 

2

Stephen Ellis, NASA
11:00, Thursday, 17 January 2008
Title: Virtual environments and the examined life: or Whatever happened to VR
Abstract:

 

1

Einar Broch Johnsen, University of Oslo
11:00, Friday 11 January 2008
Title: Modeling and Analysis in Maude
Abstract: This is an informal talk in three parts. Part one is a general discussion about the applicability and design of (formal) specification languages. Part two provides a high-level overview of Maude, a freely available, modern, and widely applicable specification language and tool. Part three gives a quick primer and demo of the use of this language and tool. As this is an informal talk, questions, comments, and discussions along the way will be most welcome.

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.