Prof. Hamideh Afsarmanesh Visited Our Group
Prof. Hamideh Afsarmanesh from University of Amsterdam visited our group and gave a talk "Semi-automated Software Service Integration in Virtual Organizations" on October 19, 2018.
To enhance business opportunities, organizations involved in many service industries are increasingly active in pursuit of both on-line provision of their business services and collaborating with others. Collaborative networks of organizations in service industry sector, however, face many challenges when it comes to sharing and especially integration of their shared business services, and corresponding software services. Catering to the need for a service interoperability framework has therefore gained momentum in research for supporting Virtual Organizations (VOs). Central to such a framework, is the requirement to support generation of formal machine-readable specification for shared business processes. Such business process specifications provide the unambiguous definitions needed for developing their counterpart software services.
A main contribution of our research involves providing concise representations for functional behavior of services, as well as applying user specified/desired service behavior for the purpose of automated matchmaking/selection of existing services in the VO breeding environment (VBE). Our proposed framework provides both a model and an implementation architecture for provision and discovery, as well as for composition of shared services. As such, it supports semi-automated development of integrated value-added services in VOs. Automated selection of most suitable service(s) incorporates service quality a spects. Service integration/composition approach applies the VO business service model, further to deploying Reo circuits and ECT tools to define complex interaction protocols and coordination among business processes that are provided by different organizations.
Details of the talk can be found here.
Prof. Farhad Arbab Visited Our Group
Prof. Farhad Arbab from Leiden University and CWI visited our group and gave a mini-course "Interaction by Composition" on October 10 and 17, 2018.
Programming language constructs and abstractions, along with techniques for their efficient compilation, have dramatically advanced in the last half-century, to the extent that today we can program at the level of (parametric) types, classes, objects, mathematical functions, monads, or Horn clauses, when appropriate, and obtain executable code whose performance competes with---indeed often beats---that of code written by competent programmers in some low-level language. Protocols constitute an equally significant abstraction in specification of concurrent applications as do functions, types, and other computational constructs, and their concrete implementation has an equally significant impact on performance and scalability of an application as that of any high-level computational construct.
In spite of significant advances in concurrency theory, constructs and models for programming of concurrent applications have essentially stagnated in the past half-century. In contrast to advances in abstractions and constructs for sequential programming, no real abstract protocol constructs have evolved. Consequently, programmers today use the same cumbersome, error-prone concurrency constructs to express protocols in modern software as they did 50 years ago: processes, threads, locks, semaphores, monitors, rendezvous, etc. The unavailability of high-level protocol constructs in contemporary programming languages hampers full utilization of the enormous potential offered by massively parallel hardware platforms in real-life applications.
In this course, we describe an interaction-centric model of concurrency that turns interaction protocols into concrete first-class mathematical objects, expressed as relations that constrain communication actions of their engaged processes. This model serves as the formal foundation for a domain-specific language (DSL), called Reo, for programming concurrency protocols. A protocol in Reo manifests itself as a connector. Complex connectors result from direct composition of simpler ones, which in turn comprise of a network of primitive binary connectors, called channels. In Reo, interaction protocols become explicit, concrete, tangible pieces of software that can be specified, verified, composed, and reused, independently of the actors that they may engage in various applications. We explore different formal semantics of Reo, its various software development support tools, and discuss compilation and optimization techniques for generating efficient executable code from high-level protocol specifications in Reo.
Details of the talk can be found here.
Dr. Renato Neves Visited Our Group
Dr. Renato Neves from Minho University visited our group and gave a talk "Compositional Semantics for New Paradigms: Probabilistic, Hybrid and Beyond" on September 12, 2018.
We introduce a generic framework to systematically investigate the features of a given computational paradigm and its possible extensions. Our motivating examples are probabilistic and hybrid programming, two recent paradigms that combine atypical primitive operations – e.g. systems of differential equations, Bernoulli trials, wait calls – with classical program constructs. By applying our framework to these two cases we list all binary program operations they possess, and show precisely when and if important axioms, such as commutativity and idempotency, hold. We also examine the possibility of incorporating notions of failure and non-determinism: we show that it is possible to combine hybrid computations with non-deterministic ones via a suitable distributive law, and that there is no monad structure on PD (the composition of the powerset functor P with the finitely supported distribution functor D) whatsoever.
Details of the talk can be found here.
Prof. Bernhard Aichernig Visited Our Group
Prof. Bernhard Aichernig from TU Graz visited our group and gave a talk "Smart Black-box Testing - Combining Model Learning and Model-based Testing" on September 10, 2018.
Testing has always been a challenge due to (1) its incompleteness by nature, (2) the lack of good specifications and (3) by its high demand for resources. With the growing complexity of the systems-under-test the situation is not likely to improve. The combination of model-learning with model-based testing offers an opportunity to master this complexity. In my talk I will introduce this line of research and report about our recent results including applications in the Internet of Things. We will cover the learning and testing of several classes of models/systems including Mealy machines, Markov decision processes and timed automata. Our goal is a natural evolution of testing: with the trend of our environment becoming "smarter", e.g. smart homes, smart cars, smart production, smart energy, our testing process needs to become smart as well. We are seeing the advent of smart testing.
Details of the talk can be found here.
Dr. Bohua Zhan Visited Our Group
Dr. Bohua Zhan from TU Munich visited our group on April 26, 2018 and gave a talk "Auto2 prover in Isabelle and its application to program verification". Details of the talk can be found here.
Dr. Gaogao Yan Visited Our Group
Dr. Gaogao Yan from ISCAS visited our group on April 11, 2018 and gave a talk "Synthesizing SystemC Code from Delay Hybrid CSP".
Prof. Yongwang Zhao Visited Our Group
Prof. Yongwang Zhao from BUAA visited our group on March 21, 2018 and gave a talk "Formal Verification of Safety-Critical Operating Systems". Details of the talk can be found here.
Dr. Gang Chen Visited Our Group
Dr. Gang Chen from CASIC visited our group on November 8, 2017 and gave a talk "Formalized Engineering Mathematics and the Next Generation of Artificial Intelligence". Details of the talk can be found here.
Prof. Fei He Visited Our Group
Prof. Fei He from Tsinghua University visited our group on November 3, 2017 and gave a talk "PSpec-SQL：Enabling Fine-Grained Control for Distrubuted Data Analytics". Details of the talk can be found here.
Prof. Luis Barbosa Visited Our Group
Prof. Luis Barbosa from Minho University visited our group from September 28 to October 8, 2017 and gave a talk "Formal Modeling in Software Design". Details of the talk can be found here.
Prof. Zhiping Shi Visited Our Group
Prof. Zhiping Shi from Capital Normal University visited our group on September 20, 2017 and gave a talk "Formalization of Mathematics in Engineering". Details of the talk can be found here.
Dr. Yu Pei Visited Our Group
Dr. Yu Pei from the Hong Kong Polytechnic University visited our group on August 7, 2017 and gave a talk "Contract-based Automated Software Testing". Details of the talk can be found here.
Zhang Xiyue Visited Singapore University of Technology and Design, 2017
A student in our group, Ms. Zhang Xiyue visited Singapore University of Technology and Design in August 2017.
The visit was hosted by Dr. SUN Jun at SUTD.
Prof. Pierre-Louis Curien Visited Our Group
Prof. Pierre-Louis Curien from University Paris 7 visited our group on June 7, 2017 and gave a talk "A Syntactic Approach to Polynomial Functors and Opertopes". Details of the talk can be found here.
Prof. Min Zhang Visited Our Group
Prof. Min Zhang from ECNU visited our group on June 7, 2017 and gave a talk "Optimizing Backbone Filtering". Details of the talk can be found here.
Dr. Yu Jiang Visited Our Group
Dr. Yu Jiang from THU visited our group on May 31, 2017 and gave a talk "Dependable Model Driven Development of CPS: From Stateflow Simulation to Verified Implementation". Details of the talk can be found here.
Dr. Wen Su Visited Our Group
Dr. Wen Su from SHU visited our group on April 5, 2017 and gave a talk "Formalizing Hybrid Systems with Event-B and the Rodin Platform". Details of the talk can be found here.
Prof. Mingsheng Ying Visited Our Group
Prof. Mingsheng Ying from UTS visited our group on March 22, 2017 and gave a talk "Toward Automatic Verification of Quantum Programs". Details of the talk can be found here.
Prof. Haifeng Wang Visited Our Group
Prof. Haifeng Wang from BJTU visited our group on March 1, 2017 and gave a talk on safety-critical software for automatic train control system. Details of the talk can be found here.
Dr. Jun Sun Visited Our Group
Dr. Jun Sun from SUTD visited our group and gave a talk "Compositional Verification of Programs " on December 6, 2016.
The answer to the question - how do we verify real programs - is perhaps already answered by how we develop programs. We know that already - abstraction, composition and hierarchy. In developing a big program, each time we focus on a component of the system and use it abstractly afterwards. In this work, we explore the idea of compositional verification which aims to do the same for verifying programs. The idea is of compositional verification is to focus on verifying one component at a time, and establish system-level property based on properties on the verified components. The challenges are twofold. Firstly, a component doesn't function on its own and thus how do we obtain minimum knowledge of the rest of the system so that the component can be verified? Secondly, how do we decide what the components are?
Prof. Zhiming Liu Visited Our Group
Prof. Zhiming Liu from SWU visited our group and gave a talk "Contract-based Model of Software Architecture in Emerging Systems " on November 21, 2016.
The sustainable development of most economies and the quality of life of their citizens largely depend on the development and application of evolutionary digital ecosystems. The characteristic features of these systems are reflected in the so called Internet of Things (IoT), Smart Cities, Cyber-Physical Systems (CPS), Systems of Human-Machine-Things, and Data Centers. Compared to the challenges in traditional ICT applications that engineers used to face, system and software development is to develop and integrate new components or subsystems, new applications and front end services that depends on the infrastructures of existing systems. This has to deal with the complexity of ever evolving architectures digital components, physical components, together with sensors and smart devices controlled and coordinated by software. The architectural components are designed with different technologies, run on different platforms and interact through different communication technologies. Software runs in these systems for data processing and analytics, computation, and intelligent control. However, the critical requirements of applications of these systems should not be compromised, and thus critical components need to be “provably correct”. In this talk we discuss, for development software in these emerging systems, the need of a foundation for the combination of traditional software engineering, AI (or knowledge-based engineering) and the emerging Big Data technologies. We show how an interface theory could play a core role in this foundation for seamless combination of different models, methods and tools for software development, AI and Big Data, as well as for system integration.
Prof. Jos Baeten Visited Our Group
Prof. Jos Baeten from CWI visited our group and gave a talk "Computability Revisited" on December 22, 2015.
Classical computability theory disregards runtime interaction completely. The strong Church-Turing thesis states that anything a computer can do can also be done by a Turing machine, given enough time and memory. This thesis is invalidated by e.g. a self-driving car, as all possibly crossing pedestrians cannot be put on the Turing tape before starting, and resulting actions cannot be postponed until after finishing. Concurrency theory gives us a proper treatment of interaction. The talk surveys what happens when computability theory is integrated with concurrency theory, which theorems remain valid and which theorems should be adapted. The Reactive Turing Machine is introduced as a model of computability with interaction.
Dr. Leslie Lamport Visited PKU
Dr. Leslie Lamport (2013 Turing Award winner) visited PKU and gave a talk "Programming should be more than coding" at Stanford center on October 30, 2015. Details can be found here.
Prof. Holger Hermanns Visited Our Group
Prof. Holger Hermanns from Saarland University visited our group and gave two talks "Concurrent Programming Education in the Post-Java Era" and "How Good is Your Embedded Design, if at all?" on October 20, 2015.
Dr. Guangdong Bai Visited Our Group
Dr. Guangdong Bai visited our group from September15 to October 15, 2015 and gave a talk "Extracting Model from Implementations of Web Authentication Protocols" on October 13, 2015.
Dr. Bai is a research fellow at National University of Singapore. His research interests mainly focus on Formal Methods on Security, Mobile Security, Web Security, and System Security.
Li Shaodong Visited Singapore University of Technology and Design, 2015
A student in our group, Mr. Li Shaodong visited Singapore University of Technology and Design in 2015.
The visit was hosted by Dr. SUN Jun at SUTD.
Ocean University of China and Qingdao University, July 2014
Sun Meng visited College of Information Science and Engineering, Ocean University of China, and College of Information Engineering, Qingdao University in July 2014.
The visit was hosted by Prof. Li Jinhua at Qingdao University and Prof. Xu Jinliang at Ocean University of China.
Two Students Visited Singapore University of Technology and Design, 2014
Two students in our group, Chen Xiaohong and Li Yi visited Singapore University of Technology and Design in 2014.
Both visits were hosted by Dr. SUN Jun at SUTD.
Sun Yat-Sen University, October 2013
Sun Meng visited School of Information Science and Technology, Sun Yat-Sen University in October 2013, and give a talk "Modeling and Verifying Connectors in Complex Systems".
The visit was hosted by Prof. Zhou Xiaocong at Sun Yat-Sen University.
Xiamen University, June 2013
Sun Meng visited Xiamen University in June 2013, and give a talk "Modeling and Verifying Connectors in Complex Systems".
The visit was hosted by Prof. Zhang Defu at Xiamen University. More information about the talk can be found here.