mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 73) Show all publications
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2019). Specification and Formal Verification of Atomic Concurrent Real-Time Transactions. In: The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018: . Paper presented at The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 04 Dec 2018, Taipei, Taiwan.
Open this publication in new window or tab >>Specification and Formal Verification of Atomic Concurrent Real-Time Transactions
2019 (English)In: The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Although atomicity, isolation and temporal correctness are crucial to the dependability of many real-time database-centric systems, the selected assurance mechanism for one property may breach another. Trading off these properties requires to specify and analyze their dependencies, together with the selected supporting mechanisms (abort recovery, concurrency control, and scheduling), which is still insufficiently supported. In this paper, we propose a UML profile, called UTRAN, for specifying atomic concurrent real-time transactions, with explicit support for all three properties and their supporting mechanisms. We also propose a pattern-based modeling framework, called UPPCART, to formalize the transactions and the mechanisms specified in UTRAN, as UPPAAL timed automata. Various mechanisms can be modeled flexibly using our reusable patterns, after which the desired properties can be verified by the UPPAAL model checker. Our techniques facilitate systematic analysis of atomicity, isolation and temporal correctness trade-offs with guarantee, thus contributing to a dependable real-time database system.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41710 (URN)
Conference
The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 04 Dec 2018, Taipei, Taiwan
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2018-12-18 Created: 2018-12-18 Last updated: 2018-12-18Bibliographically approved
de Oliveira, A. L., Paiva Bressan, L., Montecchi, L. & Gallina, B. (2018). A Systematic Process for Applying the CHESS Methodology in the Creation of Certifiable Evidence. In: 14th European Dependable Computing Conference EDCC-2018: . Paper presented at 14th European Dependable Computing Conference EDCC-2018, 10 Sep 2018, Iasi, Romania.
Open this publication in new window or tab >>A Systematic Process for Applying the CHESS Methodology in the Creation of Certifiable Evidence
2018 (English)In: 14th European Dependable Computing Conference EDCC-2018, 2018Conference paper, Published paper (Refereed)
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40869 (URN)10.1109/EDCC.2018.00019 (DOI)2-s2.0-85058374880 (Scopus ID)
Conference
14th European Dependable Computing Conference EDCC-2018, 10 Sep 2018, Iasi, Romania
Projects
AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems
Available from: 2018-09-20 Created: 2018-09-20 Last updated: 2018-12-27Bibliographically approved
Gannous, A., Andrews, A. & Gallina, B. (2018). Bridging the gap between testing and safety certification. In: IEEE Aerospace Conference Proceedings: . Paper presented at 2018 IEEE Aerospace Conference, AERO 2018, 3 March 2018 through 10 March 2018 (pp. 1-18). IEEE Computer Society
Open this publication in new window or tab >>Bridging the gap between testing and safety certification
2018 (English)In: IEEE Aerospace Conference Proceedings, IEEE Computer Society , 2018, p. 1-18Conference paper, Published paper (Refereed)
Abstract [en]

DO-178C and its supplement DO-331 provide a set of objectives to be achieved for any development of airborne software systems when model-driven development approaches are in use. Fail-safeMBT is an academic recently proposed model-based approach for testing safety-critical systems. Fail-safeMBT is a potential innovative testing process that needs compelling arguments to be adopted for the development of aeronautical software. In this paper, we reduce the gap between industrial settings and academic settings by adopting the safety case approach and derive substantiation data aimed at arguing Fail-safeMBT compliance with the standards. We explain Fail-safeMBT processes in compliance with software process engineering Meta-Model 2.0, then apply Fail-safeMBT on the Autopilot system. Finally, we link Fail-safeMBT outputs to DO-178/DO-331 process elements, then we derive a substantiation from Fail-safeMBT outputs to support the compelling arguments for achieving certification objectives. Thus, we provide a validation of Fail-safeMBT in the avionic domain.

Place, publisher, year, edition, pages
IEEE Computer Society, 2018
Keywords
Accident prevention, C (programming language), Regulatory compliance, Software testing, Systems analysis, Airborne software, Autopilot systems, Industrial settings, Model based approach, Model driven development approaches, Safety certification, Safety critical systems, Software process engineerings, Safety testing
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-40294 (URN)10.1109/AERO.2018.8396539 (DOI)2-s2.0-85049862575 (Scopus ID)9781538620144 (ISBN)
Conference
2018 IEEE Aerospace Conference, AERO 2018, 3 March 2018 through 10 March 2018
Available from: 2018-07-26 Created: 2018-07-26 Last updated: 2018-07-26Bibliographically approved
Gallina, B. & Friedemann, B. (Eds.). (2018). Computer Safety, Reliability, and Security: 37th International Conference, SAFECOMP 2018, Västerås, Sweden, September 19-21, 2018, Proceedings. Paper presented at 37th International Conference, SAFECOMP 2018, Västerås, Sweden, September 19-21, 2018. Springer
Open this publication in new window or tab >>Computer Safety, Reliability, and Security: 37th International Conference, SAFECOMP 2018, Västerås, Sweden, September 19-21, 2018, Proceedings
2018 (English)Conference proceedings (editor) (Other academic)
Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41723 (URN)10.1007/978-3-319-99130-6 (DOI)978-3-319-99130-6 (ISBN)
Conference
37th International Conference, SAFECOMP 2018, Västerås, Sweden, September 19-21, 2018
Projects
AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems
Available from: 2018-12-21 Created: 2018-12-21 Last updated: 2018-12-21Bibliographically approved
Gallina, B., Skavhaug, A. & Bitsch, F. (Eds.). (2018). Computer Safety, Reliability, and Security: SAFECOMP 2018 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Västerås, Sweden, September 18, 2018, Proceedings. Paper presented at SAFECOMP 2018 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Västerås, Sweden, September 18, 2018. Springer
Open this publication in new window or tab >>Computer Safety, Reliability, and Security: SAFECOMP 2018 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Västerås, Sweden, September 18, 2018, Proceedings
2018 (English)Conference proceedings (editor) (Other academic)
Place, publisher, year, edition, pages
Springer, 2018
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41722 (URN)10.1007/978-3-319-99229-7 (DOI)978-3-319-99228-0 (ISBN)978-3-319-99229-7 (ISBN)
Conference
SAFECOMP 2018 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Västerås, Sweden, September 18, 2018
Projects
AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems
Available from: 2018-12-21 Created: 2018-12-21 Last updated: 2018-12-21Bibliographically approved
Alajrami, S., Romanovsky, A. & Gallina, B. (2018). Cost-Aware Scheduling of Software Processes Execution in the Cloud. In: Proceedings of the 6th International Conference on Model-Driven Engineering and Software Development - Volume 1: . Paper presented at 6th International Conference on Model-Driven Engineering and Software Development MODELSWARD-2018, 22 Jan 2018, Funchal, Madeira, Portugal (pp. 203-212).
Open this publication in new window or tab >>Cost-Aware Scheduling of Software Processes Execution in the Cloud
2018 (English)In: Proceedings of the 6th International Conference on Model-Driven Engineering and Software Development - Volume 1, 2018, p. 203-212Conference paper, Published paper (Refereed)
Abstract [en]

Using cloud computing to execute software processes brings several benefits to software development. In a previous work, we proposed a reference architecture, which treats software processes as workflows and uses cloud computing to execute them. Scheduling the execution in the cloud impacts the execution cost and the cloud resources utilization. Existing workflow scheduling algorithms target business and scientific (data-driven) workflows, but not software processes workflows. In this paper, we adapt three scheduling algorithms for our architecture and propose a fourth one; the Proportional Adaptive Task Schedule algorithm. We evaluate the algorithms in terms of their execution cost, makespan and cloud resource utilization. Our results show that our proposed algorithm saves between 19.74% and 45.78% of the execution cost and provides the best resource (virtual machine) utilization compared to the adapted algorithms while providing the second best makespan. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-38619 (URN)10.5220/0006607902030212 (DOI)2-s2.0-85052027409 (Scopus ID)978-989-758-283-7 (ISBN)
Conference
6th International Conference on Model-Driven Engineering and Software Development MODELSWARD-2018, 22 Jan 2018, Funchal, Madeira, Portugal
Projects
AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems
Available from: 2018-03-06 Created: 2018-03-06 Last updated: 2018-08-30Bibliographically approved
Cai, S., Gallina, B., Nyström, D. & Seceleanu, C. (2018). Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems. In: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018: . Paper presented at 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 30 Oct 2018, Limassol, Cyprus (pp. 355-374).
Open this publication in new window or tab >>Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems
2018 (English)In: 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 2018, p. 355-374Conference paper, Published paper (Refereed)
Abstract [en]

Concurrency control faults may lead to unwanted interleavings, and breach data consistency in distributed transaction systems. However, due to the unpredictable delays between sites, detecting concurrency control faults in distributed transaction systems is difficult. In this paper, we propose a methodology, relying on model-based testing and mutation testing, for designing test cases in order to detect such faults. The generated test inputs are designated delays between distributed operations, while the outputs are the occurrence of unwanted interleavings that are consequences of the concurrency control faults. We mutate the distributed transaction specification with common concurrency control faults, and model them as UPPAAL timed automata, in which designated delays are encoded as stopwatches. Test cases are generated via reachability analysis using UPPAAL Model Checker, and are selected to form an effective test suite. Our methodology can reduce redundant test cases, and find the appropriate delays to detect concurrency control faults effectively.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41709 (URN)10.1007/978-3-030-03424-5_24 (DOI)978-3-030-03424-5 (ISBN)
Conference
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2018, 30 Oct 2018, Limassol, Cyprus
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2018-12-20 Created: 2018-12-20 Last updated: 2018-12-20Bibliographically approved
Castellanos Ardila, J. P., Gallina, B. & UL Muram, F. (2018). Enabling Compliance Checking against Safety Standards from SPEM 2.0 Process Models. In: The Euromicro Conference on Software Engineering and Advanced Applications SEAA 2018: . Paper presented at The Euromicro Conference on Software Engineering and Advanced Applications SEAA 2018, 29 Aug 2018, Prague, Czech Republic.
Open this publication in new window or tab >>Enabling Compliance Checking against Safety Standards from SPEM 2.0 Process Models
2018 (English)In: The Euromicro Conference on Software Engineering and Advanced Applications SEAA 2018, 2018Conference paper, Published paper (Refereed)
Abstract [en]

Compliance with process-based safety standards may imply the provision of a safety plan and its corresponding compliance justification. The provision of this justification is time-consuming since it requires that the process engineer checks the fulfillment of hundred of requirements by taking into account the evidence provided by the process entities. Available methodologies and their implemented tools can be used to automate this checking and provide a compliance report that can be part of the justification to be scrutinized by the safety auditor. In this paper, we explain our compliance checking vision for supporting the process engineer, in which the interaction between SPEM 2.0 (Software & Systems Process Engineering Metamodel) and Regorous (a tool-supported methodology for compliance checking) is established. Then, we focus on SPEM 2.0 to identify mechanisms to provide the minimal set of elements required to be processed by Regorous and describe how to implement them in EPF Composer. We also illustrate these mechanisms by modeling a simple example from ISO 26262 and show how a compliance report can be used to trace unfulfilled requirements.

Keywords
Compliance checking, SPEM 2.0, Regorous.
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40853 (URN)10.1109/SEAA.2018.00017 (DOI)000450238900008 ()2-s2.0-85056477430 (Scopus ID)
Conference
The Euromicro Conference on Software Engineering and Advanced Applications SEAA 2018, 29 Aug 2018, Prague, Czech Republic
Projects
AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems
Available from: 2018-09-18 Created: 2018-09-18 Last updated: 2019-01-04Bibliographically approved
Capilla, R., Gallina, B. & Cetina, C. (2018). Foreword. In: Lect. Notes Comput. Sci.: . Paper presented at 21 May 2018 through 23 May 2018. Springer Verlag
Open this publication in new window or tab >>Foreword
2018 (English)In: Lect. Notes Comput. Sci., Springer Verlag , 2018Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Verlag, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10826 LNCS
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-39368 (URN)2-s2.0-85047133208 (Scopus ID)9783319904207 (ISBN)
Conference
21 May 2018 through 23 May 2018
Note

Conference code: 213459; Export Date: 31 May 2018; Editorial

Available from: 2018-05-31 Created: 2018-05-31 Last updated: 2018-05-31Bibliographically approved
Castellanos Ardila, J. P. & Gallina, B. (2018). Formal Contract Logic Based Patterns for Facilitating Compliance Checking against ISO 26262. In: CEUR Workshop Proceedings, Volume 2049: . Paper presented at 1st Workshop on Technologies for Regulatory Compliance TeReCom-2017, 13 Dec 2017, Luxembourg, Luxemburg (pp. 65-72).
Open this publication in new window or tab >>Formal Contract Logic Based Patterns for Facilitating Compliance Checking against ISO 26262
2018 (English)In: CEUR Workshop Proceedings, Volume 2049, 2018, p. 65-72Conference paper, Published paper (Refereed)
Abstract [en]

ISO 26262 demands a confirmation review of the safety plan, which includes the compliance checking of planned processes against safety requirements. Formal Contract Logic (FCL), a logic-based language stemming from business compliance, provides means to formalize normative requirements enabling automatic compliance checking. However, formalizing safety requirements in FCL requires skills, which cannot be taken for granted. In this paper, we provide a set of ISO 26262-specific FCL compliance patterns to facilitate rules formalization. First, we identify and define the patterns, based on Dwyer' et al.'s specification patterns style. Then, we instantiate the patterns to illustrate their applicability. Finally, we sketch conclusions and future work.

Series
CEUR Workshop Proceedings, ISSN 1613-0073
Keywords
ISO 26262, Confirmation review, Compliance checking, Formal Contract Logic, Safety compliance patterns
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-38647 (URN)2-s2.0-85045562240 (Scopus ID)
Conference
1st Workshop on Technologies for Regulatory Compliance TeReCom-2017, 13 Dec 2017, Luxembourg, Luxemburg
Projects
AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems
Available from: 2018-03-02 Created: 2018-03-02 Last updated: 2018-05-11Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-6952-1053

Search in DiVA

Show all publications