|
Seminars and Colloquia 2009 |
| [24] |
|
| Speaker: |
Thomas Anung Basuki
|
| Time: |
11:00, Tuesday 17 November 2009
|
| Venue: |
UNU-IIST Seminar Room
|
| Title: |
Modelling a Biological Population: the Aedes Albopictus Case Study
|
| Abstract: |
Modelling biological systems is a challenging research topic. Biological systems range from microscopic systems such as a cell, to macroscopic systems such as a population of animals or an ecosystem. Each system offers different challenges in modelling and analysis. In this seminar, we present a model of Aedes albopictus population. Aedes albopictus is a species of mosquito which is known as a vector of many diseases. A model of Aedes albopictus population can be used to better understand the population dynamics by means of analysis techniques such as simulation and model-checking. Later on, in silico experiments such as human approaches to control the population can be performed and evaluated. We model the Aedes albopictus population dynamics using Calculi of Looping Sequences, a class of formalisms that has been successfully used to model biological systems at molecular and cellular level.
|
| Slides: |
Download Slides |
| [23] |
|
| Speaker: |
Markus Roggenbach, Swansea University, UK |
| Time: |
15:00, Thursday 22 October 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Towards Testing from CSP-CASL |
| Abstract: |
In this talk, we present a theory for the evaluation of test cases with respect to formal specifications. In particular, we use the specification language CSP-CASL to define and evaluate black-box tests for reactive systems. Using loose semantics and three-valued test oracles, our approach is well-suited to deal with the refinement of specifications. In a structured development process of computational systems, abstract specifications are gradually refined into more concrete ones. With our approach, it is possible to develop test cases already from very abstract and basic specifications, and to reuse them later on in more refined systems. |
| Biography: |
Markus Roggenbach is Senior Lecturer for Computer Science at Swansea University, Wales, UK. His research interests are Formal Methods, with a special interest in Process Algebra, Algebraic Specification, Testing, and Tools. He is a member of the IFIP WG 1.3 on Foundations of System Specification.
He did his Master Degree at Karlsruhe University (TH), Germany, received his PhD from Mannheim University, Germany. He then worked as a postdoc in the group of B Krieg-Brueckner at Bremen University, Germany, before
in 2003 he became a lecturer at Swansea University. |
| [22] |
|
| Speaker: |
Zhao Liang |
| Time: |
15:00-15:15, Monday 14 September 2009 |
| Venue: |
UNU-IIST Basement
|
| Title: |
Graph and graph transformation for object-oriented and service-oriented systems |
| Abstract: |
Graph theories form an important part of the mathematical foundations of computing, and have been applied in a wide range of areas from algorithms design and analysis to models of static structure and dynamic behavior of computer systems and programs. As a brief introduction of the research topics for my PhD study, this presentation talks about how graphs and graph transformations can be used in modeling the states and behavior of object-oriented and service-oriented systems. |
| [21] |
|
| Speaker: |
Stefan Jaehnichen |
| Time: |
11:00, Monday 14 September 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Brain Computer Interfacing |
[20]
|
|
Speaker:
|
Thomas Anung Basuki |
| Time: |
11:00, Thursday 20 August 2009 |
Venue:
|
UNU-IIST Seminar Room |
Title:
|
Modelling Cell Cycle at Different Levels of Representation |
Abstract:
|
Understanding the behaviour of biological systems requires a complex setting of in vitro and in vivo experiments, which attracts high costs in terms of time and resources. The use of mathematical models allows researchers to perform computerised simulations of biological systems, which are called in silico experiments, to attain important insights and predictions about the system behaviour with a considerably lower cost. Computer visualisation is an important part of this approach, since it provides a realistic representation of the system behaviour. We define a formal methodology to model biological systems using different levels of representation: a purely formal representation, which we call molecular level, models the biochemical dynamics of the system; visualisation-oriented representations, which we call visual levels, provide views of the biological system at a higher level of organisation and are equipped with the necessary spatial information to generate the appropriate visualisation. We choose Spatial CLS, a formal language belonging to the class of Calculi of Looping Sequences, as the formalism for modelling all representation levels. We illustrate our approach using the budding yeast cell cycle as a case study.
|
| [19] |
|
| Speaker: |
Tahiry Rabehaja |
| Time: |
15:00, Monday 20 July 2009
|
Venue:
|
UNU-IIST Seminar Room |
Title:
|
Refinement Algebra with Explicit Probabilism
|
Abstract:
|
The study of probabilistic algorithms was first motivated by their efficiency with respect to their non-probabilistic counterparts. In general, the running time of a randomized algorithm is evaluated on average (rather than in its worst case) and the probability for the worst case running time is very small. Such phenomena permit application of randomized algorithms to security. In fact, the (natural) hypothesis made here is that an adversary is unable to guess the outcome of a coin flip unless the coin has already been flipped. Further motivation for the study of randomized algorithms is their syntactic simplicity. Unfortunately it is in general hard to analyse their performance.
We give an algebraic framework for the study of probabilistic computations. A first-order axiom system is given in which we have full control of probabilities. We then prove that the normal-form theorem for standard programs extends to probabilistic programs: any probabilistic program can be simulated by a program with at most one loop. Since it is impossible to replicate in an exact way the information flow in one execution of a randomized program, the number of steps made by the original loop and the normal form may differ; but it is believed that the average number of steps is conserved by the transformation to normal form. We also study the theoretical foundation of our axiomatization. We give mathematical models, constructed from the usual semantics of probabilistic programs, to ensure the axioms are sound. Finally, another benefit of the axioms is the first-order property. This suggests automation of proofs in the algebra by means of automated theorem provers (or other tools).
|
Slides:
|
Download Slides
|
| [18] |
|
| Speaker: |
Manohar K Bhattarai, Vice Chairman, High Level Commission for IT Government of Nepal, Singhdurbar, Kathamandu, Nepal |
| Time: |
11:00, Wednesday 24 June 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Leveraging ICTs for Broader Policy Outcomes: Prospects and Challenges for Nepal |
| Abstract: |
With a very low per capita GDP and a population growth hovering around 2% a year, Nepal's developmental challenges are indeed formidable. However, despite the persistence of a protracted conflict situation over the last decade, Nepal was nonetheless able to make considerable progress toward reducing poverty, with, for example, the headcount poverty rate falling dramatically from 42 percent to 31 percent between FY95/96 and FY03/04.
In order to ensure political stability and come out of precarious political situation that it is currently in, Nepal must sustain poverty reduction. In this context, Nepal faces the dual challenges of accelerating domestic growth and sharing this growth more broadly across the population. Policies to achieve these ends will help all citizens of Nepal including groups that have been traditionally excluded. There is, therefore an invariable need to further stimulate economic growth and mount innovative responses that seek to address growing aspirations of the people.
It is along these lines that Nepal has been putting great emphasis on exploring ways and means of effectively capitalizing on the assumed transformative potentials of ICTs. A key policy question is do ICTs really hold the promise of making up for the shortcomings in governance and service delivery in a developing country scenario / can they be tools for development and growth?
Past few years have seen increased awareness about the possible roles that ICTs could play in Nepal's development strategies. The manifestations of this awareness have reflected both in community led initiatives (establishment of rural telecentres) as well as in government domain in Nepal. Some definitive policy posturing on part of the government have led to relatively faster growth of ICT sector and ICT uptake across the Nepali socio-economic spectrum is on the rise. The opening up of telecom and Value added services sector in 2004, for example, have resulted in increased teledensity, proliferations of ISPs and overall internet footprint. Recently, Nepal has embarked upon an ambitious initiative with the launching of the first phase of eGovernment project.
Being largely a mountainous country, ICTs indeed offer a lot of hope for Nepal. As a sizable section of the population remains isolated from government mainstream on account of geographical barriers, ICTs have surfaced as an effective medium for ensuring participation and inclusion. IT enabled implementations like telemedicine, distance education, wireless applications, the use of the Internet for a wide variety of critical information dissemination tasks hold the promise of overcoming fundamental barriers of infrastructure which characterize challenges faced by Nepal.
The fact remains nonetheless that Nepal has still to go a long way before being able to fully capitalize on pontentialities offered by ICTs. For one, the resourcefulness of ICTs in the context of a developing country scenario can only be capitalized on the presence of an ecosystem favourable to the growth of the sector. Confronted with a set of competing priorities, the government finds itself in a difficult position when in comes to allocating resources for really crucial infrastructure projects, for example, like broadband network rollout.
The presentation will take stock of current ICT scenario of Nepal including some initiatives that are currently underway. Discussions will also centre around as to what opportunities do exist for aligning potentialities and resourcefulness offered by ICTs towards realization of broader policy outcomes.
|
| KEYWORDS: |
IT, ICTs, digital divide, development, growth, service delivery |
| BIOGRAPHY: |
Mr. Bhattarai's experience in IT domain spans more than two decades having started out his career as a computer programmer and systems analyst in the year 1985. Serving currently as the Vice Chairman of High Level Commission for IT, an apex level IT policy and strategy outfit chaired by the Prime Minister of Nepal, Mr. Bhattarai has wide ranging experience of working both for the public and the private sector.
Mr. Bhattarai played a key role in drafting Nepal's first IT Policy in the year 2000 as part of a team formed by National Planning Commission, Government of Nepal. More significantly, Mr. Bhattarai is credited with the initiative to usher in the concept of rural telecentres in Nepal as a means of bridging digital divide and expanding community access to ICTs in the country after having launched first rural ICT kiosk at a village called Bhimphedi in the year 2000 with the financial support from UNDP. He has been involved in designing a number of capacity development programmes and community engagement models aimed at enhancing community level capacities to effectively leverage resourcefulness offered by information and communications technologies within the broad context of development and poverty reduction strategies.
Mr. Bhattarai has, of late, also been involved in preparing revised IT Policy and drafting 3-year integrated action plan (IAP) for the development of ICT sector in Nepal. In addition, he also played a key role as the leader of project preparatory technical assistance team in developing ICT development project through the support of ADB which has since culminated in a comprehensive, 30MN US$ project being executed through Office of Prime Minister and Council of Ministers (OPMCM), Government of Nepal. Mr. Bhattarai retains a strong professional interest in harnessing ICTs for development and in exploring ways and means of strengthening fundamentals of good governance through digital means. |
| [17] |
|
| Speaker: |
Rafael Carvalho |
| Time: |
11:00, Thursday 4 June 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Simulation of Cell Proliferation |
| Abstract: |
Cells represent the main units of which living beings are made. One important property of the cell is the ability to reproduce themselves by cell division, in which a mother cell generates two daughter cells. The process by which a cell duplicates itself, grows, and prepares to divide again to generate new cells is called cell cycle. In this seminar we present and demonstrate a graphical tool to simulate and visualise in three dimension the cell cycle. Chemical reactions occurring within the cell are modelled using Spatial CLS (Calculus of Looping Sequences), a formal language for biological systems, which is based on rewrite logic. The tool visualises in three dimensions the effect of such chemical reactions on the cell cycle. |
| [16] |
|
| Moderator: |
Mr. Remi Chandran, Senior Researcher, UNU-IIST Center for Electronic Governance. |
| Time: |
10:00 - 11:30, Friday 22 May 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Electronic Environmental Governance - Importance, Challenges and the Way Forward |
| Abstract: |
As the different UN biodiversity-related conventions each impose reporting requirements on their parties and also stress the need for environmental compliance related information, meeting these requirements can place substantial burden on governments, particularly those with limited resources. A feasibility study conducted by UNEP-World Conservation Monitoring Centre in 1998 considered approaches towards development of a harmonized information management infrastructure for the treaties within their existing mandates. Its purpose was to consider how the secretariats could improve effectiveness and efficiency in gathering, handling, disseminating and sharing information. As a first step in enabling this process, there is a need for information flow to a national repository from a grass root level.
On the occasion of the World Biodiversity Day, UNU-IIST Center for Electronic Governance will contribute to the global discussion on effective monitoring and evaluation of global compliance to multilateral environmental agreement through Information and Communication Technologies, through a panel discussion. The panel will also examine the issue regarding harmonizing of environmental law enforcement related information for strengthening Environmental Governance.
The panelists will include stakeholders from Government, Research Institutions, Industry, Civil Society and the United Nations. |
| Panelists: |
Mr. A.N. Prasad, Inspector General of Forests (IGF), Ministry of Environment and Forests, Government of India, New Delhi
Ms. Aschta Nita Boestani, Assistant Senior Officer, ASEAN-Wildlife Enforcement Network, Bangkok
Mr. Alexander de Sherbinin , Deputy Manager, Earth Institute, Columbia University, New York.
Dr. Adegboyega Ojo: Research Fellow, UNU-IIST.
Mr. Peter Eredics, Manager, ESRI, Redlands, California
Dr. Aster Li Zhang, Programme Director, Conservation International - China
Ms. Onkuri Majumdar, Programme Officer- Freeland Foundation, Bangkok. |
| [15] |
|
| Speaker: |
Professor Wei Zhao, Rector of the University of Macau |
| Time: |
15:00 to 17:00, Tuesday 19 May 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Camouflaging Technologies in Cyber Space |
| Abstract: |
For many Internet applications, the ability to protect the identity of participants and the characteristics of their communication in distributed applications is critical. For such applications, a number of traffic camouflaging systems have been developed over the past several years. The effectiveness of these systems relies greatly on (1) the protocol by which messages are (re-)routed among the participants and (2) the scheme by which links are padded. In this talk, we will discuss our recent discoveries on the effectiveness of these camouflaging methods. Our results contradict some of the methods that have been commonly used. For example, we find that using more agents in re-routing may not necessarily increase the probability that a sender can be identified. Furthermore, padding links with a constant-bit rate pattern may result in the worst probability; that an adversary can identify the underlying payload status. We will discuss how to develop optimal strategies for these traffic camouflaging systems. |
| Biography: |
Internationally renowned Chinese-American scholar Professor Wei Zhao has been appointed the eighth Rector of the University of Macau (UM) commencing on 10 November 2008. At the same time as taking up the new rectorship, he is also appointed the first Chair Professor of the University of Macau. Professor Zhao completed his undergraduate programme in physics at Shaanxi Normal University, Xi'an, China, in 1977, and he later received his MSc and PhD degrees in Computer and Information Sciences at the University of Massachusetts at Amherst, in 1983 and 1986 respectively. Before joining the University of Macau, Professor Zhao served as the Dean of the School of Science at Rensselaer Polytechnic Institute, Director for the Division of Computer and Network Systems in the US National Science Foundation, and Senior Associate Vice President for Research at Texas A&M University. During his academic career, he has also worked as a faculty member at Shaanxi Normal University, Amherst College, University of Adelaide, Texas A&M University, and Rensselaer Polytechnic Institute.
As an IEEE Fellow, Professor Zhao has made significant contributions in distributed computing, real-time systems, computer networks, and cyberspace security. His research group has been well recognized and received numerous awards and prizes including the outstanding paper award from the IEEE International Conference on Distributed Computing Systems, the best paper award from the IEEE National Aerospace and Electronics Conference, and an award on technology transfer from the Defense Advanced Research Program Agency. In 2007, he received the IEEE Transactions on Parallel and Distributed Systems Outstanding Achievement Award. Professor Zhao is the holder of two US patents and has published over 280 papers in journals, conferences, and book chapters.
Since the 1980s, hundreds of thousands of Chinese students have travelled to America to work and study, but very few attained such high achievements as Professor Zhao, who served as senior research and education administrator in the US comprehensive universities and a senior official of a US federal government agency. Meanwhile, Professor Zhao continues to engage actively in various activities for education and research exchange with the People's Republic of China. He was the founding chair of the US-China Dragon Star Committee, Overseas Advisory Committee for Shanghai Jiaotong University Electronics and Information Technology College, and Overseas Advisory Committee for the Higher Education Press (in the field of Computer Science). In 2005, he was awarded the Lifelong Achievement Award by the Chinese Association of Science and Technology (CAST USA). In 2007, he was honored with the Overseas Achievement Award by the Chinese Computer Federation.
Professor Zhao shows great passion for higher education. He looks forward to working closely with administrators, faculty, staff, and students to elevate the University's position in the international community. With the support of the Macao SAR Government, he is confident to build on the University's strengths and enhance its international reputation, making the University of Macau a leading university in the country and beyond. |
| [14] |
|
| Speaker: |
Dr. Marc Levy, Deputy Director Center for International Earth Science Information Network (CIESIN) Earth Institute, Columbia University New York |
| Time: |
10:30 to 11:30, Thursday 21st May 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
The Information Underpinnings of the Sustainability Transition: Priorities, Gaps and Strategies |
| Abstract: |
Navigating the transition toward sustainable development requires making a number of changes in business as usual practices. A number of these changes have attracted a great deal of attention, such reductions in pollution fluxes, reductions in resource consumption, changes in land use practices, and shifts in the distribution of political power. A less well-appreciated, but equally important, element of the sustainability transition concerns information. I will characterize the information needs of the sustainability transition, drawing insights from recent experiences with sustainability indicators, scenario analysis, risk assessment, and early warning. I will then identify priority information needs for the sustainability transition, assess information gaps, and outline a strategy aimed at creating an information infrastructure to address core needs. |
| Biography: |
Marc Levy is Deputy Director of the Center for International Earth Science Information Network (CIESIN), part of the Earth Institute at Columbia University. He also serves as an adjunct professor in Columbia's School of International and Public Affairs. He is a political scientist specializing in the human dimensions of global change. He is an expert on environment-security connections, environmental sustainability, emerging infectious diseases, the geography of poverty, and the effectiveness of international environmental institutions. His work has been supported by a large number of national and international agencies. He serves as Lead Project Scientist of the Socioeconomic Data and Applications Center; and directs the Earth Institute of Cross-Cutting Initiative on Environment-Security Linkages. He has served on a number of global environmental assessments and frequently advises national governments and international organizations on global change issues. Before coming to CIESIN in 1998 Mr. Levy had teaching appointments at Princeton University and Williams College.
Contact: marc.levy@ciesin.columbia.edu
http://www.ciesin.columbia.edu/levy.html |
| [13] |
|
| Speaker: |
Dr. ir. Marijn Janssen (Associate Professor Program Director SEPAM Delft University of Technology The Netherlands) |
| Time: |
15:00, Tuesday 26 May 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Enterprise Architectures and Network Orchestration |
| Abstract: |
Given the fragmented nature of public administration, there is a need to integrate the various services and orchestrate them in a coherent manner. Orchestration is the effective coordination of the dependencies among various organizations. The orchestration of cross-organizational processes requires changes at the technology, application, information and business process level. In this presentation an overview of orchestration, its role and enterprise architecture development will be given. |
| Biography: |
Dr. Marijn Janssen is an Associate Professor within the Information and Communication Technology Section and Director of the interdisciplinary SEPAM Master programme of the Faculty of Technology, Policy and Management at Delft University of Technology. He has been a consultant for the Ministry of Justice and received a Ph.D. in information systems (2001). He serves on several editorial boards and is involved in the organization of a number of conferences. He published over 140 refereed publications.
More information: http://www.tbm.tudelft.nl/marijnj. |
| [12] |
|
| Speaker: |
MICHAEL ADENIYI AKINGBADE |
| Time: |
15:00, Monday 13 April 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Model-checking Atomic Register Algorithms Using CSP/FDR2 |
| Abstract: |
This first part of the work is an extensive survey of existing algorithms on atomic registers. Different algorithms are classified and organised into a `cube' according to the strength of atomicity the algorithms can achieve. In the second part we select four interesting algorithms in the cube and model them using CSP. Three of them are successfully verified using refinement check of FDR2. It shows that model-checking is useful in understanding and verifying small but tricky concurrent algorithms like those for atomic register construction. |
| [11] |
|
| Speaker: |
Davide Gualerzi Department of Economic Sciences "Marco Fanno" Università di Padova, Italy(davide.gualerzi@unipd.it) |
| Time: |
11:00, Monday 30 March 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
The Internet and the Economy |
| Abstract: |
The large question of the effects of the Internet on the economy can be approached from many angles. The impact of the Internet is a topic in the Economics of Information technologies or Industrial economics. It may lead to consider more specific questions, such as the problems and prospects of E-Commerce or the success stories of Internet companies such as Google. More in general it leads to consider the meaning of the New Economy associated with the 1990s economic expansion and that of the Information economy.
These topics are all aspects of the "coming of age of Information technologies" (Gualerzi, D. The coming of Age of Information Technologies and the Path of Transformational Growth. A long term perspective on the current recession. London, Routledge. Forthcoming) that reached its peak in the US during the 1990s.
However, the impact of the Internet is analyzed in the broader perspective of a network effect by which the combination of information processing with telecommunications determines the possibility of increasing returns and qualitative change. Qualitative change takes the form of restructuring of productive processes and entire industries, and the rise of new ones, of new products and services, thus a process of structural change. The development of networks, and of the Internet in particular, is the fundamental novelty of the 1990s and the key to the transformation exemplified by the so-called "new economy". The technology frenzy and the stock market bubble, which eventually led to the collapse of the expansion, followed.
The point is that the key to the transformation is not the computer but the network, not the effects on productivity of Information Technologies but the market creation prospects of ICTs products and the Internet.
The particular angle from which the question is analyzed is precisely that of the relationship between technology development and macro performance during the 1990s expansion of the US economy. That affords an insight on the causes of the recession of the late 2000s and its long term prospects. |
| Biography: |
Davide Gualerzi is Associate Professor, Department of Economic Sciences "Marco Fanno", School of Political Sciences, University of Padua. Visiting Scholar, Department of Economics, New School University, New York, USA. Researcher. I.S.P.E. (Istituto studi per la programmazione economica), Rome. Assistant Professor of Economics. Bard College. Annandale-on-Hudson, N.Y.
Education: 1991 Ph.D. Economics. The Graduate Faculty of Political and Social Science, New School for Social Research, New York. 1978-79 Post-graduate annual course in management of the economy and of the firm. ISTAO (Istituto A. Olivetti), Ancona, Italy. 1978 Laurea in Urbanistica. IUAV (Istituto Universitario di Architettura di Venezia), School of Urban Planning, Venice, Italy. |
| [10] |
|
| Speaker: |
Prof. Wojciech Cellary Department of Information Technology Poznan University of Economics (www.kti.ue.poznan.pl/) |
| Time: |
11:30, Friday 20 March 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Economic Dilemma of the Knowledge-Based Economy |
| Abstract: |
The lecture deals with the dilemma followed from the double character of knowledge. On the one hand, knowledge is an individual and social good that determines the quality of life. On the other hand, knowledge is an economical good, a funding concept for the Knowledge-Based Economy. The dilemma is: should knowledge be for free or paid? It is argued that the achievement of Knowledge (Information) Society without Knowledge-Based Economy is impossible. A compromise approach to financing knowledge development is proposed, motivated by the need for sustainable development of economy as a precondition for social welfare. This approach consists of the public financing only a precisely defined part of the knowledge sector: first, the knowledge that does not develop any more, and second, the knowledge necessary to bring new social groups to the knowledge-based economy. |
| Biography: |
Prof. Wojciech Cellary is a computer scientist, head of the Department of Information Technology at the Poznan University of Economics. In his professional career he worked at nine universities in Poland, France, and Italy. His research interests are currently focused on internet technologies, multimedia, electronic business and economy, electronic government and information society. He is an author of 10 books and over 100 scientific papers. He gives lectures on electronic business to over 700 students per year. He was a leader of many scientific and industrial projects. He served as a consultant to several Polish ministries, Polish Parliament and Senate, as well as European Commission. He was scientific editor of the report at Poland and the Global Information Society: Logging once developed under auspices of United Nations Development Programme. |
| [9] |
|
| Speaker: |
Andreas Griesmayer |
| Time: |
15:00, Wednesday 18 March 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Dynamic symbolic execution for concurrent systems |
| Abstract: |
We extend dynamic symbolic execution to distributed and concurrent systems. Dynamic symbolic execution can be used in software testing to systematically identify equivalence classes of input values and has been shown to scale well to large systems. Although usually restricted to sequential programs, this scalability makes it interesting to consider the technique in the distributed and concurrent setting as well. In order to extend the technique to concurrent systems, it is necessary to obtain sufficient control over the scheduling of concurrent activities to avoid race conditions. Creol, a modeling language for distributed concurrent objects, solves this problem by abstracting from a particular scheduling policy but explicitly defining scheduling points. This provides sufficient control to apply the technique of dynamic symbolic execution for model based testing of interleaved processes. The technique has been formalized in rewriting logic, executes in Maude, and applied to non-trivial examples, including an industrial case study. |
| Slides: |
Download slides |
| [8] |
|
| Speaker: |
Rudi Schlatte |
| Time: |
15:00, Monday 16 March 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Modeling and Testing Multi-Threaded Asynchronous Systems with Creol |
| Abstract: |
Modeling concurrent systems and testing multi-threaded implementations against the model is an exciting field of study. I will present work done on constructing and executing test cases for an industrial-size multi-threaded application against a model written in the Creol modeling language. Models written in Creol, an object-oriented, concurrent modeling language, can be structurally similar to the finished implementation; we show how to keep this desirable property when re-using Creol models as test oracles. Also, a conformance relation between model and system under test that needs less controllability than other relations that are based on automata is presented. |
Slides:
|
Download slides |
| [7] |
|
| Speaker: |
Dr. Vincent Oria, Department of Computer Science,the New Jersey Institute of Technology |
| Time: |
11:00, Thursday March 5 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Mining Lecture Videos for slides: An Approach to Semantic Querying of lecture videos |
| Abstract: |
Pattern matching in the video is challenging especially if the patterns have to reflect some semantics. The aim of this work is to synchronize a sequence of slides with the video of the lecture that used the same slides. Knowing where a particular slide appears in a lecture video can help index the video based on the slides and find where a particular topic is covered. Another application for this work is live video conferences where matching a slide in a live video with the actual slide can help replace the poor quality slide in the video with a slide previously downloaded. Although the problem of pattern matching in video is not new and has already been tackled, existing methods are designed for general purpose pattern matting and turn out to be very expensive and time consuming. In this paper, we define the similarity ratio as a measure for quickly matching the video frame with the original slide. The slide with the highest similarity ratio is the most likely match. The experiments show encouraging results. |
| Biography: |
Vincent Oria is an associate professor of computer science at the New Jersey Institute of Technology. He got a Bachelor and a Master degree in Computer Science from the Institut National Polytechnique of Cote d'Ivoire respectively in 1983 and 1989 and a PhD from the Ecole Nationale Superieure des Telecommunications (ENST), Paris, France in 1994. From 1996 to 1999 he was a post-doctoral fellow at the University of Alberta Canada before joining NJIT in January 2000. His research interests are multimedia databases, database issues in e-learning, moving object databases, database security recommender systems and social networks. He has held visiting professor positions at different institutions including the Chinese University of Hong-Kong (China), the National Institute of Informatics, (Tokyo, Japan), FhG-IPSI (Darmstadt, Germany), ENST (Paris, France), University of Paris-IX Dauphine (Paris, France), INRIA (Roquencourt, France) , CNAM (Paris France) and the University of Versailles St Quentin (Versailles, France). He has served on a number of multimedia and database conference program committees. |
| Slides: |
Download slides |
| [6] |
|
| Speaker: |
Shaofa Yang, UNU-IIST |
| Time: |
11:00, Wednesday 25 February 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
The MSO Theory of Connectedly Communicating Processes |
| Abstract: |
We identify a network of sequential processes that communicate by synchronizing frequently on common actions. More precisely, we demand that there is a bound k such that if the process p executes k steps without hearing from process q and directly or indirectly and then it will never hear from q again. The non-interleaved branching time behavior of a system of connectedly communicating processes (CCP) is given by its event structure unfolding. We show that the monadic second order (MSO) theory of the event structure unfolding of every CCP is decidable. Using this result, we also show that an associated distributed controller synthesis problem is decidable for linear time specifications that do not discriminate between two different linearizations of the same partially ordered execution. This is joint work with P. Madhusudan and P.S. Thiagarajan. |
| Biography: |
Shaofa Yang is currently a post-doctoral fellow at UNU-IIST, funded by the PEARL project. He obtained his Bachelor, Master's and Ph.D. (2006) degrees in computer science from National University of Singapore. Prior to coming to UNU-IIST, he was a post-doctoral fellow at INRIA-Rennes, France. His research interests include formal methods relevant to concurrent systems, real-time and hybrid systems. |
| [5] |
|
| Speaker: |
Einar Broch Johnsen, University of Oslo, Norway (joint work with Johan Dovland, Olaf Owe, and Martin Steffen) |
| Time: |
11:00, Wednesday 18 February 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Lazy Behavioral Subtyping |
| Abstract: |
Late binding allows flexible code reuse but complicates formal reasoning significantly, as a method call’s receiver class is not statically known. This is especially true when programs are incrementally developed by extending class hierarchies. Lazy behavioral subtyping is a novel method to reason about late bound method calls. In contrast to traditional behavioral subtyping, reverification is avoided without restricting method overriding to fully behavior-preserving redefinition. The approach ensures that when analyzing the methods of a class, it suffices to consider that class and its superclasses. Thus, the full class hierarchy is not needed, and incremental reasoning is supported. We formalize this approach as a calculus which lazily imposes context-dependent subtyping constraints on method definitions. The calculus ensures that all method specifications required by late bound calls remain satisfied when new classes extend a class hierarchy. The calculus does not depend on a specific program logic, but the examples use a Hoare-style proof 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. |
| Slides: |
Download slides |
| [4] |
|
| Speaker: |
Jirarat Sitthiworachart, Walailak University, Thailand |
| Time: |
11:00, Wednesday 11 February 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Computer support of effective peer assessment in an undergraduate programming class |
| Abstract: |
Active learning is considered by many academics as an important and effective learning strategy. Assessment is integrated in learning as a tool for learning, but traditional assessment methods often encourage surface learning (passive learning) rather than deep learning (active learning). Peer assessment is a method of motivating students, involving students discussing, marking, and providing feedback on other students at work, and is one of the successful approaches which can be used to enhance deep learning. Students are required to think critically about what they are learning during the peer assessment process. Tutors ’ marking is usually accepted as reliable, but student peersu’ marking in a peer assessment process is suspect. As part of a study investigating whether peer assessment can be an accurate assessment method in a computer programming course, a novel web-based peer assessment tool has been developed. We describe the tool and report the results of evaluating the tool through experiments involving large programming classes. The results suggest that computer-mediated peer assessment is a valuable assessment approach which promotes active learning and is an accurate assessment method in a programming course. |
| Biography: |
Dr Jirarat Sitthiworachart is a lecturer in the School of Informatics at Walailak University, Thailand. Her research interests include educational technology, and computer science education. Dr Sitthiworachart has master degree in Information Technology and a PhD in Computer Science from the University of Warwick, United Kingdom. |
| Slides: |
Download slides |
| [3] |
|
| Speaker: |
Magnus Myreen, University of Cambridge Computer Laboratory |
| Time: |
15:00, Wednesday 4 February 2009 |
| Venue: |
UNU-IIST Seminar Room |
| Title: |
Machine-code verification for multiple architectures - An application of decompilation into logic |
| Abstract: |
This talk presents a method, supported by a tool, for the formal verification of machine code which exposes as little as possible of the `big models' to its user. It is thus able to make non-automatic proofs independent of the models. That is achieved using a Decompiler that extracts (with proof in HOL4) a function describing the effect of the code on the model. This seminar concentrates on: what is decompilation into logic and how can such decompiliation be implemented? Biography: Magnus Myreen was an undergraduate in Oxford where he read Computer Science at Lady Margaret Hall and has just completed a DPhil at Cambridge under the supervision of Mike Gordon. For further details see http://www.cl.cam.ac.uk/~mom22/ |
|
Slides:
|
Download slides |
| [2] |
|
Speaker:
|
Zhao Liang |
| Time: |
15:30, Wednesday 21 January 2009 |
Venue:
|
UNU-IIST Basement |
| Title: |
Graphs and Transformations in Software Design - a PhD Research Proposal |
| Abstract: |
Graph theories form an important part of the mathematical foundations of computing, and they applied in a wide range of areas from algorithms design and analysis to models of static structure and dynamic behavior of computer systems and programs. In this report, we proposal a PhD research topic on the application of graphs and graph transformations in the area of software modeling and analysis, with a focus on object-oriented programs and service based programs.
|
Slides:
|
Download slides
|
[1]
|
|
Speaker:
|
Thomas Anung Basuki |
| Time: |
16:30, Tuesday 20 January 2009 |
| Venue: |
UNU-IIST Basement |
| Title: |
Statistical Model-Checking for Biological Systems |
| Abstract: |
In my thesis proposal last year, I have presented some ideas on model-checking biological systems. Now I will give some realisations of those ideas as a progress report about my thesis. In biological systems the state space is very large and makes the use of probabilistic model-checking unfeasible due to the state-explosion
problem. Statistical model-checking differs from probabilistic model-checking in the way it explores the state space. In statistical model-checking a property is checked on a sample of the state space, so preventing state-explosion. The applicability of this approach is shown by translating Stochastic CLS models into the Maude rewrite system and performing statistical model-checking. |
| Slides: |
Download slides |
|
|
Seminars and Colloquia 2009