Keynote Addresses:

Fausto Giunchiglia(University of Trento): Semantic Matching
Abstract: This talk is in two parts. In the first part I'll describe my view of how meta-data (mainly ontologies) should be organized in the semantic Web. The idea is that we should allow the use of multiple ontologies and link concepts which are semantically related. The talk will briefly describe the language that we have defined, called C-OWL, and that allows this kind of representations.
In the second part I'll describe an approach, called Semantic Matching, an algorithm and a system, called S-Match, which allows for the automatic computation of mappings/links between concepts of two ontologies/classifications.

John Mylopoulos(University of Trento, Italy and Univeristy of Toronto, Canada): Software Engineering and Agent-Oriented Modelling
Abstract: Software development methodologies (such as structured/object-oriented ones) have traditionally adopted programming concepts and used them for design and requirements analysis. We outline a novel methodology (called Tropos) where organizational concepts -- such as actor, goal and actor dependency on another actor -- are adopted and used throughout the software development process from early requirements to detailed design. The result of this methodology is agent-oriented software in the sense that components are agents and the relationships between them are social dependencies, rather than import/export ones.
The presentation sketches on-going research on the Tropos methodology, including the software development process itself, a formal specification language founded on the concepts of actor, goal and actor dependency, and formal analysis tools for different types of Tropos models. We also sketch a range of applications of the methodology, from the design of web services to the design of secure software and autonomic software systems

Paolo Traverso(ITC/IRST): Automated Composition of Web Services:Research Challenges
Abstract: Web Services provide a universal basis for the development and execution of business processes that are published over the network and available via standard interfaces and protocols. Service Composition is one of the most promising idea underlying web services: composed web services perform new functionalities by interacting with pre-existing services that are published on the Web. One of the major challenges for industry-wide adoption of Web services is the automated composition of distributed business processes. i.e., the development of techniques that support an effective, reliable, low-cost, and time-efficient composition of web services.
After a discussion on some of the main research challenges, the presentation will focus on a the problem of the automated composition of executable web services: given a set of descriptions of available services, and a composition requirement, the problem is that of synthesizing automatically a process that, when executed, composes the available services by interacting with them.

Technical Program:

P N Ananth Raman: HP Initiatives: Web and Grid

S. Arun-Kumar(IIT, Delhi): Clausal Resolution in the Multi-Modal Logic of BDI Agents
Abstract: We assume that agents execute in a distributed setting and possess only limited knowledge about the environment. We assume (though whether it is realistic at all, is debatable) that each agent attempts to maintain a consistent mental state, during its execution. An important problem in the theory of multi-agent systems is that of of revision of the mental state of an agent during its execution, when it receives fresh information from the environment. One important proof technique to determine inconsistency is resolution. Resolution methods do exist for the unimodal logics of S4, S5, T and K.
We present a resolution technique for multi-modal logics of Belief, Goal and Intention using resolution at different levels of a tree of clauses, where each such tree represents the mental state of a single agent. The use of resolution is to determine the inconsistency within the tree. We have considered belief and goal as modal logic operators satisfying the KD45? and KD axioms respectively. Intention is not considered a separate modality, but is instead defined based on beliefs and goals. We also have proofs of soundness and completeness of the logic. Keywords: Modal logic, Multi-agent systems, Resolution, Proof method.

Anup Bhattacharya(BARC): Semantics of UML 2 Activity Charts

Soumen Chakrabarti(IIT, Mumbai): Breaking through the syntax barrier: searching with entities and relations
Abstract: The next wave in search technology will be driven by the identification, extraction, and exploitation of real-world entities represented in unstructured textual sources. Search systems will either let users express information needs naturally and analyze them more intelligently, or allow simple enhancements that add more user control on the search process. The data model will exploit graph structure where available, but not impose structure by fiat. First generation Web search, which uses graph information at the macroscopic level of inter-page hyperlinks, will be enhanced to use fine-grained graph models involving page regions, tables, sentences, phrases, and real-world-entities. New algorithms will combine probabilistic evidence from diverse features to produce responses that are not URLs? or pages, but entities and their relationships, or explanations of how multiple entities are related.

R.K. Joshi(IIT, Mumbai): Early Aspects in Agent Oriented Modelling
Abstract: Aspect orientated extensions to object oriented programming languages have enabled separation of concerns through primitives that go beyond core object oriented primitives. We believe that the research in aspect oriented paradigms will help in evolving paradigms for capturing cross-cutting concerns in other phases of life-cycle, more specifically to requirements capture. In this talk, we will present preliminary results on extensions to agent-oriented models based on TROPOS for capturing aspects early in software life cycle.

Kalyansundaram(TIFR, Mumbai): formal verification of pipelined processors

Neerav Karnik(IBM):Grid Computing: Service Oriented Perspective

Manu Kuchchal (IBM): Autonomic Computing

Kamal Lodaya(IMSC, Chennai): Interval Temporal Logic

Fabio Massacci(University of Trento): Interactive Access Control for Autonomic Communication and Business Processes
Abstract: Controlling access to services is a key aspect of Web Services and the last few years have seen the domination of policy-based access control. The intuition is that actions of nodes ``controlling" the communication are automatically derived from policies. Policies can be ``simple'' event-action rules for Linux firewalls or complex logical policies expressed in languages such as Ponder.
Abstracting away the details of the policy implementation, we can observe that only one reasoning service is actually used by policy based self-management: deduction. Given a policy and a set of additional facts and events, we find out all consequences (actions or obligations) of the policy and the facts, i.e.\ whether granting the request can be deduced from the policy and the current facts.
One of the problem for Web services is that no partner may guess a priori what kind of credentials will be sent by clients and clients may not know a priori which credentials are required for completing a business process. So Web Services needs at least another reasoning service: abduction.
Loosely speaking, abduction is deduction in reverse: given a policy and a request for access to services, find the credentials/events that would grant access, i.e. a (possibly minimal) set of facts that added to the policy would make the request a logical consequence.
In this talk we will show a logical framework for reasoning about access control for Web services based on answer set programming. Our model is based on interaction and exchange of requests for supplying or declining missing credentials between two partners each of them possibly running his/hers interactive access control algorithm.

Fabio Massacci(University of Trento): Modelling Security and Trust for an Agent Oriented Software Engineering Methodology
Abstract: The last years have seen a number of proposals to incorporate Security Engineering into mainstream Software Requirements Engineering. However, capturing trust and security requirements at an organizational level (as opposed to a design level) is still an open problem.
This course presents a formal framework for modeling and analyzing security and trust requirements. The presented framework shows how to extend the i*/Tropos methodology, a state-of-the-art agent-oriented software engineering methodology, with trust and security requirements. The key intuition is that in modeling security and trust, we need to distinguish between the actors that manipulate resources, accomplish goals or execute tasks, and actors that own the resources or the goals.
To analyze an organization and its information systems, we proceed in two steps. First, we built a trust model, determining the trust relationships among actors, and then we give a functional model, where we analyze the actual delegations against the trust model, checking whether an actor that offers a service is authorized to have it.
The formal framework allows for the automatic verification of security and trust requirements by using a suitable delegation logic that can be mechanized within Answer Set programming.
To make the discussion more concrete, we illustrate the proposal with a real case study based on the ISO17799? compliance of the Univ. of Trento and people may play with our CASE Tool.

H.M. Mohanty(University of Hyderabad): Business Process Modelling: Trends and Challenges
Abstract: Developments in both computer and communication technologies have initiated widespread automation of corporate activities. At initial stages isolated business functionalities were automated in order to accomplish a task of faster pace. Later, the automation is intended to achieve a business goal that is possible only by efficient execution of tasks that leads to the goal. This requirements has lead to a branch of study called business process reengineering. Existing business activities of a corporation are to be modeled, simulated and refined to achieve business goals. Business process modeling is an active area of research. A chain of activities of a business is modeled as work flow. i.e., a composition of activity primitives. Later petri nets, event process chain and most recently UML techniques are being used for the purpose. Other than functionalities the factors like time and resource utilizations are also being considered in business modeling. As inter-organizational and social issues are vital for success of business activities, researchers argue to bring these into the gamut of modeling. In this talk I will survey on different techniques proposed for business modeling and identify challenges involved in it.

K. Narayan Kumar(CMI, Chennai): Netcharts: Bridging the gap between HMSC and executable specifications.

N.V. Narendra Kumar(TIFR, Mumbai): Security Protocols: Modelling and Analysis

P.K. Pandya(TIFR, Mumbai): Monitoring Scenario-based specification using Interval Duration Logic
Abstract: Message Sequence Charts (MSC) provide an inter-object view of scenarios arising in a distributed system execution. Live Sequence Charts (LSC) are a formal notation based on MSC for specifying behaviour of a distributed system. They allow properties such as possibility and necessity of some scenarios in system execution to be formulated. In this talk, we first formalize LSC-like specifications into an interval tempopral logic, QDDC. Using the automata theoretic decision procedure for logic QDDC, we show how monitors can synthesized for verifying the validity of LSC specification in a system run. We also consider model checking of the LSC specifications, and automatic synthesis of systems satisfying such LSC specifications.

Marco Pistore(University of Trento): Planning via Model Cheching
Abstract: Planning under uncertainty is one of the most significant and challenging planning problems. Most realistic applications need to deal with uncertainty about the domain and the environment, and to deal with incomplete knowledge at planning time and partial observability at execution time. The problem of planning under uncertainty has been shown to be hard, both theoretically and experimentally. "Planning via Model Checking" is a general and well-founded approach to planning under uncertainty. In the talk we descrive this planning approach and show how it applies to a wide range of planning domains with undertainty, including planning in non-deterministic domains, planning with partial information available at run time, and planning for requirements expressed in temporal logic.

Marco Pistore(University of Trento): A Theoretical Framework for Web Service Composition
Abstract: Web services are an emerging technology that enables the interoperability among distributed, web-accessible software components. One of the most interesting opportunities provided by web services is service composition, that is, the possibility of assembling pre-existing services in order to provide new functionalities. However, a wide adoption of web service composition requires the development of new techniques and tools supporting the design and execution of the composed services. In this talk we describe a theoretical framework that allows for modeling web services and their compositions, and that supports functionalities such as formal verification, automated synthesis, and monitoring of composed services. The key aspect of the framework is that it provides a model of web service interactions which is at the same time faithful wrt existing service execution engines and abstract wrt the actual communication mechanisms, thus allowing for an efficient verification, synthesis, and monitoring.

Krithi Ramamritham(IIT, Mumbai): A formal framework for advanced transactional applications
Abstract: Electronic commerce systems (retail, auction, etc.) are good examples of data-based systems that operate under correctness and resilience requirements of a transactional nature but go beyond conventional databases, as they are formed by the aggregation of heterogeneous, autonomous components. In this talk we introduce a framework to specify, analyze, and reason about the behavior of such systems, focusing on how they are designed to make consistent progress in spite of failures. The framework allows the hierarchical composition of transactional systems and their properties, as well as the proofs of these properties: we specify a system's behavior at its most abstract level, and proceed to decompose the specification mirroring the structure of the system's components, considering the role of guarantee-preserving component systems and recovery in each case. In particular, we show how the lower-level properties are supported by the component systems, which we also characterize within the same framework.

S. Ramesh(IIT, Mumbai): Formal Verification Opportunities in Automotive Software

Luciano Serafini(ITC/IRST): Distributed Reasoning in ontology spaces
Abstract: The talk addresses the problem of reasoning with multiple ontologies interrelated with semantic mappings. This problem is becoming more and more relevant due to the necessity of building a scalable ontological reasoning tools for the Semantic Web.
In contrast to the so called global approach, in which reasoning with multiple semantically related ontologies is performed in a global knowledge base that encodes both ontologies and semantic mappings, we propose a distributed reasoning approach in which reasoning is the result of combination via semantic mappings of local reasonings chunks performed in single ontologies.
The paper presents a tableau-based distributed reasoning procedure which is sound and complete w.r.t. Distributed Description Logics, the formal framework used to represent multiple semantically connected ontologies. I will brievly describe the design and implementation principles of a distributed reasoning system, called DRAGO (Distributed Reasoning Architecture for a Galaxy of Ontology), that implements such distributed decision procedure.

R.K. Shyamasundar(TIFR, Mumbai): TBA

Biplav Srivastava(IBM): Towards End-to-End Composition of Web Services
Abstract: The demand for quickly delivering new applications is increasingly becoming a business imperative today. Application development is often done in an ad hoc manner, without standard frameworks or libraries, thus resulting in poor reuse of software assets. Web services have received much interest in industry due to their potential in facilitating seamless business-to-business or enterprise application integration. A web services composition tool can help automate the process, from creating business process functionality, to developing executable workflows, to deploying them on an execution environment. However, we find that the main approaches taken thus far to standardize and compose web services are piecemeal and insufficient. The business world has adopted a (distributed) programming approach in which web service instances are described using WSDL, composed into flows with a language like BPEL and invoked with the SOAP protocol. Academia has propounded the AI approach of formally representing web service capabilities in ontologies, and reasoning about their composition using goal-oriented inferencing techniques from planning. At IBM IRL, we have developed the first integrated work in composing web services end to end from specification to deployment by synergistically combining the strengths of the above approaches.
In this talk, I will discuss the motivations, issues and the implemented solution for end-to-end web service composition. We present the prototype service creation environment along with a use-case scenario, and demonstrate how it can significantly speed up the time-to-market for new services.

Angelo Susi(ITC/IRST): TBA -- Tropos

G.V. Uma(Anna University, Chennai): Restructuring Natural Languages Text to elicit requirements capture
Abstract: Application of natural language understanding to requirements gathering remains a field that has only limited explorations so far. Further, automation of requirements gathering process is a field that still needs improvisation. This text describes an approach for automatic requirements capture. This approach starts by segmenting the requirements discourse text followed by identification of parts of speech from the text by sentence tagging techniques. The text thus parsed is restructured into subject-verb-object pattern on which the pronoun and the co-reference resolutions are carried on. Finally the object-oriented elements of the system are identified based on which use-case and class diagram constituents are captured thus eliciting requirements gathering.

Satish Vadhyar (IISC): Grid Computing Architecture

P. Venkat Rangan: Wireless Sensor Networks and their Applications

Adolfo Villafiorita(ITC/IRST): Business process modelling in UML

Click here for abstracts