Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops: ASYDE, CIFMA, and CoSim-CPS, Amsterdam, The Netherlands, September 14–15, ... (Lecture Notes in Computer Science, 12524)

Preface
Contents
ASYDE 2020
	Organization
	ASYDE 2020 – Workshop Chairs
	ASYDE 2020 – Programme Committee
	ASYDE 2020 – Steering Committee
Model Translation from Papyrus-RT into the nuXmv Model Checker
	1 Introduction
	2 Case Studies
	3 Translation Approach
		3.1 UML-RT State-Diagrams to Finite-State-Machines
		3.2 Translation into SMV Model
		3.3 Model Restrictions
	4 Evaluation
	5 Related Work
	6 Conclusion and Future Work
	References
Modeling and Verification of Temporal Constraints for Web Service Composition
	1 Introduction
	2 Motivation Scenario
	3 Temporal Constraints Modeling and Verification
	4 TCPN-Based Modeling
	5 CPN Tools-Based Monitoring
	6 Java Framework-Based Evaluation
	7 Conclusion
	References
Modeling Attack-Defense Trees' Countermeasures Using Continuous Time Markov Chains
	1 Introduction
	2 ADTrees and CTMCs
		2.1 ADTrees
		2.2 Enumerated Continuous Time Markov Chains
		2.3 Countermeasures in ADTrees
		2.4 CTMC Model for Countermeasures
		2.5 Tokenized Continuous Time Markov Chain
	3 Tokenized-CTMC for Countermeasure Modeling
	4 Conclusion
	References
Automated Validation of State-Based Client-Centric Isolation with TLA+
	1 Introduction
	2 Background: State-Based Client-Centric Consistency
	3 Formalizing CI in TLA+
	4 CI Examples
	5 Model Checking Algorithms Using CI
		5.1 Formalizing 2PL/2PC
		5.2 Model Checking 2PL/2PC
		5.3 2PL/2PC Bug Seeding
	6 Discussion and Future Work
	7 Conclusion
	References
Code Coverage Aware Test Generation Using Constraint Solver
	1 Introduction
	2 Background
	3 The Proposed Method
		3.1 Determining Parameter Weight
		3.2 Test Case Generation
	4 Experimental Evaluation
	5 Conclusion
	References
From Requirements to Verifiable Executable Models Using Rebeca
	1 Introduction
	2 The Door Controller Case Study
	3 Structured Requirements
	4 The Architecture
	5 The Mapping from Requirements to Behavioral Models
		5.1 The Mapping to Logical Properties
	6 The Behavioral Models
		6.1 Formal Verification
	7 Discussion and Future Work
	8 A Quick Overview of Related Work
	References
CIFMA 2020
	Organization
	CIFMA 2020 – Workshop Chairs
	CIFMA 2020 – Programme Committee
	CIFMA 2020 – Additional Reviewers
A Pragmatic Model of Justification for Social Epistemology
	1 Introduction
	2 Communitarian Epistemology
	3 The Role of Conditionals for Human Discursive Practices
	4 The Dimensions of Justification
	5 Conclusion
	References
Personal Identity and False Memories
	1 Introduction
	2 Experimental Data
	3 Evaluation and Discussion
	4 Conclusion
	References
Against the Illusory Will Hypothesis
	1 Introduction
	2 The Experience of Causal Relations
	3 The I Spy Experiment
	4 The Causal Experience in the I Spy Experiment
	References
Understanding Responses of Individuals with ASD in Syllogistic and Decision-Making Tasks: A Formal Study
	1 Introduction
	2 The Syllogistic Task
		2.1 Computational Level Analysis (Syllogistic Task)
		2.2 Algorithmic Level Analysis (Syllogistic Task)
	3 The Decision Task
		3.1 Computational Level Analysis (Decision Task)
		3.2 Algorithmic Level Analysis (Decision Task)
	4 Discussion
	5 Future Work
	References
Symbolic and Statistical Theories of Cognition: Towards Integrated Artificial Intelligence
	1 Introduction: MIT's AI Lab, Now and Then
	2 The Fundamental Tension Between Symbolic and Statistical Paradigms of Cognition
		2.1 Maxwell's Dualistic View of Nature
		2.2 The Chomsky Versus Norvig Debate on the Nature of Science and Cognition
		2.3 A Manifestation of the Fundamental Tension in Natural Language Semantics
	3 Towards Integrated Artificial Intelligence and Integrated Cognitive Science
		3.1 The Integrated Paradigm: A Classification of Integrated AI
		3.2 Five Features of Integrated AI: Making AI More Verifiable, Explainable, Accountable, Ethical, and Thus More Human
	4 Concluding Remarks: The Integrated Paradigm as a Transdisciplinary Trading Zone
	References
An Interdisciplinary Model for Graphical Representation
	1 Introduction
	2 Data-Driven and Problem-Driven Models
	3 Research Questions and Hypotheses
	4 Case Studies Evaluation
		4.1 Descriptive Case Studies
		4.2 Prescriptive Case Studies
	5 An Interdisciplinary Model
	6 Conclusion and Future Works
	References
Information Retrieval from Semantic Memory: BRDL-Based Knowledge Representation and Maude-Based Computer Emulation
	1 Introduction
		1.1 Real-Time Maude
	2 Natural Language Constructs: Facts and Questions
		2.1 Facts
		2.2 Questions
		2.3 Modelling Facts and Question in Real-Time Maude
	3 Human Memory Model
		3.1 Fact Representation in Semantic Memory
		3.2 Short-Term Memory (STM) Model
		3.3 Human Memory as a Maude Class
	4 Experimental Environment and Its Evolution
		4.1 Modelling Perceptions
		4.2 Planning Experiments
		4.3 Environment Evolution
	5 Tick Rewrite Rules for Information Retrieval
	6 Conclusion and Future Work
	References
A Multi-Agent Depth Bounded Boolean Logic
	1 Introduction
	2 Multi-Agent DBBL
	3 Semantics
	4 Proof-Theory
	5 Meta-theory
	6 Conclusions and Future Work
	References
The Intensional Structure of Epistemic Convictions
	1 Axiomatic Setup
	2 Avoiding Logical Omniscience
	3 Individual Structuring of Convictions
	4 The Question ``Why?''
	References
Short-Circuiting the Definition of Mathematical Knowledge for an Artificial General Intelligence
	1 Introduction
	2 Idealized AGIs
	3 An Elegant Definition of Mathematical Knowledge
		3.1 Non-circularity of Definition 1
		3.2 Sentences Using the Knowledge Operator
		3.3 A Simpler Definition, and Why It Does Not Work
	4 Quantified Modal Logic
	5 Translating Knowledge Formulas
	6 Conclusion
	References
Reasoning About Ignorance and Beliefs
	1 Introduction
	2 Logic for Ignorance and Beliefs
		2.1 Defining the Formal Framework
	3 Misbelieving, Being Agnostic or Doubting
		3.1 From Misbelieving to Ignoring
		3.2 From Being Agnostic to Ignoring
		3.3 From Doubting to Ignoring
		3.4 From Ignoring to the Three Effects
	4 Hierarchies of Ignorance
	5 The Birth of Second-Order Ignorance
	6 Conclusion and Future Works
	A Formal Proofs
	References
CoSIM-CPS 2020
	Organization
	CoSim-CPS 2020 – Workshop Chairs
	CoSim-CPS 2020 – Programme Committee
A Case Study on Formally Validating Motion Rules for Autonomous Cars
	1 Introduction
		1.1 Related Work
	2 Challenges in Implementing Safety Rules Around Car Motion Control
	3 IVEX Tools Suite and Approach to Model Safety Rules for Car Motion
	4 Case Study of a SAE Level 3, Low Speed Motion Control Safety Rules Set
		4.1 Notes Regarding Real-Time Performance
	5 Conclusion
		5.1 Next Steps
	References
Modelling Train Driver Behaviour in Railway Co-simulations
	1 Introduction
	2 Background
		2.1 Co-simulation
		2.2 Human Behaviours
	3 Driver Behaviour Model
		3.1 Baseline vs. Defensive Driving
		3.2 Response Time
		3.3 Fatigue
	4 Railway Co-simulation
	5 Results
	6 Conclusions
	References
Cross-level Co-simulation and Verification of an Automatic Transmission Control on Embedded Processor
	1 Introduction
	2 Related Work
	3 Background
		3.1 PVS, Emucharts, and PVSio-web
		3.2 INTO-CPS
		3.3 SESAM/VPSim Environment
	4 Cross-level Modelling, Co-simulation and Verification
		4.1 Development Process
		4.2 Emulation of Processors with VPSim
	5 Automatic Transmission Control Case Study
		5.1 High-Level Virtual Prototyping
		5.2 Co-simulation with VPSim
		5.3 Results and Discussion
	6 Conclusions
	References
A Semantic-Aware, Accurate and Efficient API for (Co-)Simulation of CPS
	1 Introduction
	2 Problem Statement and Related Work
	3 Proposition
	4 Case Study
	5 Discussion
	6 Conclusion
	References
An FMI-Based Initialization Plugin for INTO-CPS Maestro 2
	1 Introduction
	2 Background
		2.1 FMU Definitions
		2.2 INTO-CPS Maestro 2
	3 Calculation of an Initialization Order
		3.1 Method to Calculate the Initialization Order
		3.2 Optimization of a Initialization Procedure
		3.3 The Complete Initialization Strategy
	4 Case Study
	5 Realization of a Maestro 2 Plugin
		5.1 Realization of the Topological Sorting
		5.2 Verification of the Initialization Order
	6 Related Work
	7 Concluding Remarks
	References
Introducing Regression Tests and Upgrades to the INTO-CPS Application
	1 Introduction
	2 Background
	3 Introducing Regression Tests
	4 Upgrading the Dependencies
	5 Concluding Remarks and Future Work
	References
Cosimulation-Based Control Synthesis
	1 Introduction
	2 Control Synthesis of Switched Systems
		2.1 Switched Systems
		2.2 Controller Synthesis Algorithm
	3 Set-Based Cosimulation
		3.1 Interval Analysis
		3.2 Cosimulation of Reachable Sets
		3.3 Discussion on Meta-parameters
	4 Experiments
		4.1 Case Study
		4.2 Experimental Results
		4.3 Discussion
	5 Conclusion
	References
Author Index