SAC is offering 4 half-day tutorials on Monday April 8, 2019. Tutorials are open for registered attendees. Handouts will be available online right before the conference. No printed handouts are provided during the tutorials. Please bring your copies of the handouts (printed or electronic). Lunch tickets will be issued for attendees who registered for the Tutorials Luncheon. For questions or inquiries about the tutorials, please contact the Tutorials Chair(s):
| 9:00am |
T#1 Verification of Business Process Models using Semantic Specifications Hermann Kaindl AM Coffee Break |
T#3 Formal Verification for an Internet of Secured Things Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue AM Coffee Break |
|
| 12:30pm | Social Luncheon for attendees who registered for the Tutorials Luncheon. The luncheon event will be held at the conference venue, and lunch tickets will be issued. |
||
| 14:30pm |
T#2 Architecting Software-intensive Systems on the Internet-of-Things with SysADL Flavio Oquendo PM Coffee Break |
T#4 Specifying Requirements through Interaction Design Hermann Kaindl PM Coffee Break |
|
Abstract:
We discovered a mismatch between verification and validation of even very simple business processes based on service composition and using semantic service specification. In more in-depth studies, we found that it is due to different business context of applying these services. Hence, we introduced semantic task specification for specifying tasks in their respective business context, where a specific semantic task specification may become a supertype of the corresponding semantic service specification, and this can be recursively applied to higher-level semantic task specifications in business processes. Such semantic task specifications can be utilized for formal verification of traditionally represented business process models (e.g., through control flows defined in BPMN), where they semantically annotate the (BPMN) tasks. This verification through model checking determines whether time logic formulas specifying certain properties are violated (or not) in a behavioral business process model. The semantic task specifications facilitate the systematic derivation of such a behavioral model. It integrates object life cycle models with behavioral models derived from task-centric (BPMN) models, where the integration is done by use of semantic task specifications. Formalizing business rules through properties referring to object life cycles rather than directly to task-centric models has the advantage of decoupling and potential reuse for several business models. In effect, this verification can show that a business rule is fulfilled and, indirectly, that the corresponding semantic task specifications correctly define their business context. Such a formal verification of a business process based on, e.g., Web-services, can actually verify business software implementing such a business process on this process level. It is facilitated both by semantic service specifications and the newly introduced semantic task specifications.
Bios:
Hermann Kaindl joined the Institute of Computer Technology at TU Wien in Vienna, Austria, in early 2003 as a full professor. Prior to moving to academia, he was a senior consultant with the division of program and systems engineering at Siemens Austria. There he has gained more than 24 years of industrial experience in software development and human-computer interaction. He has published five books and more than 220 papers in refereed journals, books and conference proceedings. He is a Senior Member of the IEEE and a Distinguished Scientist Member of the ACM, and he is on the executive board of the Austrian Society for Artificial Intelligence. He has previously held tutorials at CAiSE’00, RE’01, RE’02, HICSS-36, INCOSE’03, RE’03, CADUI-IUI’04, INCOSE’04, RE’04, HICSS-38, IRMA’05, INCOSE’05, AAAI’06, HCI’06, OOPSLA’06, HICSS-40, ICONS’07, INCOSE’07, AAAI’07, IFIP Interact’07, OOPSLA’07, HICSS-41, ICCGI’08, RE’08, ICSEA’08, ICIW ’09, IFIP Interact’09, SMC’09, HICSS-43, ACHI’10, eics’10, ICSEA’10, TdSE’10, HICSS-44, SAC’11, INCOSE’11, AAAI’11, RE’11, ICSEA’11, HICSS-45, SAC’12, ACM CHI’12, PROFES’12, BCS HCI’12, APSEC'12, HICSS-46, SAC’13, NexComm’13, PROFES’13, ICSOFT’13, IEEE Africon’13, IEEE APSEC’13, HICSS-47, ACM SAC’14, WEB’14, SMC’14, PROFES’14, HICSS-48, ACM SAC’15, RCIS’15, RE’15, ICCGI’15, HICSS-49, ICSR’16, SMC’16, APSEC’16, RCIS’17, eics’17, SSBSE’17, ICWI’17, ER’17, ICEIS’18 & ENASE’18, CAiSE’18, RE’18 and SPLC’18. In addition, Hermann Kaindl organized and chaired several panels at major conferences, such as the one at CHI 2001 “Methods and Modeling: Fiction or Useful Reality?”, as well as the one at RE’08 entitled “How to Combine Requirements Engineering and Interaction Design?”.
Abstract:
Software architecture has become a major discipline on applied computing, playing a key role in the specification of software-intensive systems, in particular in dynamic contexts where not only structure but also behavior needs to be addressed. In this tutorial, we present the SysADL language and the SysADL Studio tool providing both theoretical concepts and practical examples in a systematic approach to architectural design software-intensive systems on the Internet-of-Things. SysADL is a specialization of the ISO & OMG SysML Standard to software architecture description. It brings together the expressive power of architectural concepts following the ISO/IEC/IEEE 42010 framework with a standard language used by the industry. SysADL has a rigorous operational semantics, which allows the analysis and execution of the software architecture. It is organized according to three integrated viewpoints: (i) structural; (ii) behavioral; and (iii) executable. The structural viewpoint describes the main building blocks of the software architecture from a conceptual point of view, while the behavioral viewpoint is concerned with the dynamic behavior of the architecture. The behavioral viewpoint has a precise operational semantics that describes the behavior using semantically defined actions, it allows the execution of the behavior by simulation, as well as supports verification. In this tutorial, we apply SysADL Studio to illustrate the concepts and to allow attendees to gain practical experience in modeling software architecture on the Internet-of-Things and executing modeled architectures for validation. In this tutorial, the audience will learn: (i) the concepts that provide the foundation for software architectural specification and model execution using SysADL; (ii) how to design a complete software architecture using SysADL Studio and a step-to-step running example. This tutorial targets software professionals and students and it is supported by a book (Oquendo, Flavio; Leite, Jair; Batista, Thais: Software Architecture in Action: Designing and Executing Architectural Models with SysADL Grounded on the OMG SysML Standard, Springer, 2016, https://www.springer.com/us/book/9783319443379) and accompanying tool (available at www.sysadl.org).
Bios:
Flavio Oquendo is Full Professor of Computing at the University South Brittany, France, and leading Principal Investigator on Software Architecture at the IRISA Research Institute (UMR CNRS 6074, https://www.irisa.fr/en). He received the degrees of PhD and HDR (Research Direction Habilitation) in Computing from the University of Grenoble, France. He has been working with Software Architecture for more than 30 years. He has been Scientific Director of key European Projects on Software Architecture in cooperation with the industry and founding chair of the French and European Conferences on Software Architecture. He has served on Program Committees of over 100 International Conferences, including ICSA, ECSA, ICSE, ESEC/FSE, SoSE, ICECCS, ICSP and has chaired 10 of them. In particular, he has been the Program Chair of the French, European, and IEEE/IFIP conferences on Software Architecture. He has also been Guest Editor of a dozen journal special issues on Software Architecture and related fields. He has acted as referee for over 20 International Journals, including TSE, TOSEM, JSS, Oxford The Computer J. He has published over 150 refereed international journal and conference papers in Computing, being listed among the most prolific authors in the DBLP Computer Science Bibliography. His research interests are centered on rigorous languages, techniques, and tools to support the efficient architecture and engineering of software-intensive systems and their applications in industrial settings, in particular over the course of the last decade on the Internet-of-Things.
Abstract:
Connected devices and services, also referred to as the Internet of Things (IoT), are becoming more and more popular. These devices are now used in many security-critical domains. Moreover, even in non-critical domains, privacy issues may arise with devices collecting and transmitting a lot of personal information. It is therefore important to provide security guarantees for the software executed by these devices. This kind of guarantees can be brought using formal verification. In this tutorial, we describe several formal verification techniques and present them by applying Frama-C, a platform for the analysis of C programs, to verify IoT software. We illustrate it on several examples taken from Contiki, a lightweight operating system for Internet of Things. Participants will learn how to use the different Frama-C analyzers and how to combine them. Several examples and use cases presented during the tutorial will give them a clear practical vision of possible usages of the underlying static and dynamic analyses in their everyday work.
Bios:
Allan Blanchard obtained his PhD in Computer Science from the University of Orléans in 2016. He prepared his PhD at the Software Reliability Laboratory of the CEA LIST. He is interested in the analysis of concurrent code using formal methods and more precisely deductive verification. His current work, in the EU H2020 VESSEDIA project, is to apply formal verification to the Contiki microkernel and its libraries, mostly to show the absence of runtime errors. He mostly uses Frama-C with the EVA and WP plugins. He is the author of an online tutorial on deductive verification with Frama-C and its WP plugin. Web site: https://allan-blanchard.fr
Nikolai Kosmatov got a PhD in Mathematics in 2001 jointly from Saint-Petersburg State University and University of Besançon. He works as an expert researcher-engineer at CEA List. His research interests include software testing, formal verification, combinations between static and dynamic analysis techniques and runtime verification. He co-authored two patents and more than 50 scientific papers in international conferences and journals. He is the main author of the online testing service pathcrawler-online.com and contributed to the development of several other tools. Nikolai organized several international events (TAP 2015 conference, CP meets Verification workshop at CP 2016, CSTVA workshop at CP 2017, USE workshop at ICST 2018), as well as several successful tutorials on testing and verification (at iFM, ISSRE, ASE, SAC, TAP, HPCS, RV, ICTSS, ZINC, TAROT). He is co-responsible of the working group on software testing (MTV2) of the French CNRS network on software engineering (GDR GPL) and organizes its annual workshops. Web site: http://nikolai.kosmatov.free.fr
Frédéric Loulergue obtained his PhD in Computer Science from the University of Orléans in 2000 and his Habilitation in Computer Science from Université Paris Val-de-Marne in 2004. He is currently a full professor at Northern Arizona University, Flagstaff, USA. His research interest are the practical and formal aspects of the design, implementation and application, in particular to large-scale data-intensive software, of structured parallel programming languages and libraries, as well as applied formal methods and cyber security in this broad context. Software associated to his research work include Bulk Synchronous Parallel ML (BSML) and the SyDPaCC framework for the systematic development of programs for scalable computing. He co-organized the series of international workshops on High-Level Parallel Programming and Applications (HLPP) between 2003 and 2010 and is now a member of its steering committee. He created and (co)-organized the series of international workshop on Practical Aspects of High-Level Parallel Programming (PAPP) from 2004 to 2012, and the PAPP ACMSAC Track in 2016 and 2017. He co-chaired the Formal Approaches to Parallel and Distributed System (4PAD) symposium in 2016 and 2018. He is a member of the editorial board of Scalable Computing: Practice and Experience. He was associate director of the Laboratory of Algorithms, Complexity and Logic (LACL), and associate director of the Laboratoire d’Informatique Fondamentale d’Orléans (LIFO). He founded and lead the Logic Modeling and Verification (LMV) research team at LIFO (2015-16). Web site: http://frederic.loulergue.eu
Abstract:
When the requirements and the interaction design of a system are separated, they will most likely not fit together, and the resulting system will be less than optimal. Even if all the real needs are covered in the requirements and also implemented, errors may be induced by human-computer interaction through a bad interaction design and its resulting user interface. Such a system may even not be used at all. Alternatively, a great user interface of a system with features that are not required will not be very useful as well. This tutorial explains joint modeling of (communicative) interaction design and requirements, through discourse models and ontologies. Our discourse models are derived from results of human communication theories, cognitive science and sociology (even without employing speech or natural language). While these models were originally devised for capturing interaction design, it turned out that they can be also viewed as specifying classes of scenarios, i.e., use cases. In this sense, they can also be utilized for specifying requirements. Ontologies are used to define domain models and the domains of discourse for the interactions with software systems. User interfaces for these software systems can be generated semi-automatically from our discourse models, domain-of-discourse models and specifications of the requirements. This is especially useful when user interfaces for different devices are needed. Specific usability requirements can be dealt with in our approach through advanced customization approaches. Hence, interaction design facilitates requirements engineering to make applications both more useful and usable.
Bios:
Hermann Kaindl joined the Institute of Computer Technology at TU Wien in Vienna, Austria, in early 2003 as a full professor. Prior to moving to academia, he was a senior consultant with the division of program and systems engineering at Siemens Austria. There he has gained more than 24 years of industrial experience in software development and human-computer interaction. He has published five books and more than 220 papers in refereed journals, books and conference proceedings. He is a Senior Member of the IEEE and a Distinguished Scientist Member of the ACM, and he is on the executive board of the Austrian Society for Artificial Intelligence. He has previously held tutorials at CAiSE’00, RE’01, RE’02, HICSS-36, INCOSE’03, RE’03, CADUI-IUI’04, INCOSE’04, RE’04, HICSS-38, IRMA’05, INCOSE’05, AAAI’06, HCI’06, OOPSLA’06, HICSS-40, ICONS’07, INCOSE’07, AAAI’07, IFIP Interact’07, OOPSLA’07, HICSS-41, ICCGI’08, RE’08, ICSEA’08, ICIW ’09, IFIP Interact’09, SMC’09, HICSS-43, ACHI’10, eics’10, ICSEA’10, TdSE’10, HICSS-44, SAC’11, INCOSE’11, AAAI’11, RE’11, ICSEA’11, HICSS-45, SAC’12, ACM CHI’12, PROFES’12, BCS HCI’12, APSEC'12, HICSS-46, SAC’13, NexComm’13, PROFES’13, ICSOFT’13, IEEE Africon’13, IEEE APSEC’13, HICSS-47, ACM SAC’14, WEB’14, SMC’14, PROFES’14, HICSS-48, ACM SAC’15, RCIS’15, RE’15, ICCGI’15, HICSS-49, ICSR’16, SMC’16, APSEC’16, RCIS’17, eics’17, SSBSE’17, ICWI’17, ER’17, ICEIS’18 & ENASE’18, CAiSE’18, RE’18 and SPLC’18. In addition, Hermann Kaindl organized and chaired several panels at major conferences, such as the one at CHI 2001 “Methods and Modeling: Fiction or Useful Reality?”, as well as the one at RE’08 entitled “How to Combine Requirements Engineering and Interaction Design?”.