Edizione	[1st ed. 2007.]
Pubbl/distr/stampa	Berlin, Heidelberg : , : Springer, , [2007]
Descrizione fisica	1 online resource (VIII, 288 p.)
Disciplina	005.8
Collana	Lecture Notes in Computer Science
Soggetto topico	Computer security Formal methods (Computer science) Trust
ISBN	3-540-75227-7
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Strategic Games on Defense Trees -- Timed Calculus of Cryptographic Communication -- A Semantic Paradigm for Component-Based Specification Integrating a Notion of Security Risk -- Game-Based Criterion Partition Applied to Computational Soundness of Adaptive Security -- Measuring Anonymity with Relative Entropy -- Formalizing and Analyzing Sender Invariance -- From Simulations to Theorems: A Position Paper on Research in the Field of Computational Trust -- A Tool for the Synthesis of Controller Programs -- Where Can an Insider Attack? -- Maintaining Information Flow Security Under Refinement and Transformation -- A Classification of Delegation Schemes for Attribute Authority -- Program Partitioning Using Dynamic Trust Models -- Locality-Based Security Policies -- A Theorem-Proving Approach to Verification of Fair Non-repudiation Protocols -- A Formal Specification of the MIDP 2.0 Security Model -- A Comparison of Semantic Models for Noninterference -- Hiding Information in Multi Level Security Systems -- A New Trust Model Based on Advanced D-S Evidence Theory for P2P Networks.
Record Nr.	UNINA-9910484812903321

Edizione	[First edition.]
Pubbl/distr/stampa	Cham, Switzerland : , : Springer, , [2024]
Descrizione fisica	1 online resource (243 pages)
Disciplina	005.1
Collana	Lecture Notes in Computer Science Series
Soggetto topico	Component software Formal methods (Computer science) Software engineering
ISBN	3-031-52183-8
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Research Papers -- Symbolic Path-guided Test Cases for Models with Data and Time -- Model-Based Testing of Asynchronously Communicating Distributed Controllers -- A Mechanized Semantics for Component-based Systems in the HAMR AADL Runtime -- A Formal Web Services Architecture Model for Changing PUSH/PULL Data Transfer -- Joint use of SysML and Reo to specify and verify the compatibility of CPS components -- From Reversible Computation to Checkpoint-Based Rollback Recovery for Message-Passing Concurrent Programs -- Anniversary Papers -- Formal Model Engineering of Distributed CPSs using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL -- Challenges Engaging Formal CBSE in Industrial Applications -- Formal Aspects of Component Software - An Overview on Concepts and Relations of Different Theories -- Overview on Constrained Multiparty Synchronisation in Team Automata -- Embedding Formal Verification in Model-Driven Software Engineering with SLCO: An Overview.
Record Nr.	UNINA-9910800117703321

Pubbl/distr/stampa	Cham, Switzerland : , : Springer, , 2021
Descrizione fisica	1 online resource (299 pages)
Disciplina	004.0151
Collana	Lecture notes in computer science
Soggetto topico	Formal methods (Computer science)
ISBN	3-030-77867-3
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Intro -- Preface -- Organization -- Abstracts of Invited Talks -- What do the Sources Say? Exploring Heterogeneous Journalistic Data as a Graph -- Ontologies for On-Demand Design of Data-Centric Systems -- Towards Human-Guided Rule Learning -- Sustainable AI - What Does It Take for Continued Success in Deployed Applications? -- Contents -- Theory -- Representing Partition Lattices Through FCA -- 1 Introduction -- 2 Preliminaries -- 2.1 Lattices and Partitions -- 2.2 Notions of Formal Concept Analysis -- 3 Relation Between the Lattices Ln and Ln+1 -- 4 Standard Context of Ln -- References -- Fixed-Point Semantics for Barebone Relational Concept Analysis -- 1 Motivation -- 2 Preliminaries and Related Work -- 2.1 Formal Concept Analysis -- 2.2 Extending FCA -- 2.3 Relational Concept Analysis -- 2.4 RCA0 -- 3 RCA May Accept Different Concept Lattice Families: Illustration -- 4 Semantics and Properties: A Context Approach -- 4.1 The Lattice K of RCA0 Contexts -- 4.2 The Context Expansion Function F -- 4.3 Fixed Points of F -- 4.4 The Well-Grounded Semantics of RCA is the Least Fixed-Point Semantics -- 4.5 Computing the Greatest Fixed Point -- 5 Self-supported Fixed Points -- 5.1 The Lattice L of RCA0 Lattices and the Lattice Expansion Function E -- 5.2 Self-supported Lattices -- 6 Discussion -- 7 Conclusions -- References -- Boolean Substructures in Formal Concept Analysis -- 1 Introduction -- 2 Recap on FCA and Notations -- 2.1 Foundations -- 2.2 Relating Substructures in FCA -- 3 Related Work -- 4 Boolean Subcontexts and Sublattices -- 5 Closed-Subcontexts -- 6 Connecting Boolean Suborders and Boolean Subcontexts -- 6.1 Embeddings of Boolean Substructures -- 6.2 Subconcepts Associated to Suborders -- 7 Interplay of Both Approaches -- 8 Conclusion -- References -- Rules -- Enumerating Maximal Consistent Closed Sets in Closure Systems. 1 Introduction -- 2 Preliminaries -- 3 Closure Systems Given by Implicational Bases -- 4 Minimal Generators with Bounded Size -- 5 Biatomic Atomistic Closure Systems -- 6 Conclusions -- References -- A New Kind of Implication to Reason with Unknown Information -- 1 Introduction -- 2 Preliminaries -- 2.1 FCA Preliminaries -- 2.2 Attribute Implications -- 3 An Algebraic Framework for Unknown Information -- 3.1 The -semilattice of 3-sets -- 3.2 The Lattices of 4-sets and -sets -- 4 Extending the Concept of Lattice -- 5 Reasoning with Weak Implications -- 6 Conclusion and Further Work -- References -- Pruning Techniques in LinCbO for Computation of the Duquenne-Guigues Basis -- 1 Introduction -- 2 Preliminaries -- 2.1 Formal Concept Analysis, Theories, Models, and Bases -- 2.2 Duquenne-Guigues Basis -- 2.3 LinCbO -- 3 Pruning in Pseudointent Computation -- 4 How LinCbO Utilizes the Pruning -- 5 Experimental Evaluation -- 6 Our Observations -- 7 Conclusion -- References -- Approximate Computation of Exact Association Rules -- 1 Introduction -- 2 Main Definitions -- 3 Probably Approximately Correct Computation of Implications -- 4 Computing Frequency-Aware Approximations -- 5 Experimental Evaluation -- 5.1 Quality Factor -- 5.2 Testbed -- 5.3 Data Sets -- 5.4 Experiments -- 6 Conclusion -- References -- Methods and Applications -- An Incremental Recomputation of From-Below Boolean Matrix Factorization -- 1 Introduction -- 2 Problem Description -- 2.1 Non-incremental From-Below BMF -- 2.2 Incremental From-Below BMF -- 3 Incremental Algorithm -- 3.1 Adding of New Entries -- 3.2 Removing of Existing Entries -- 3.3 Time Complexity -- 4 Experimental Evaluation -- 4.1 Datasets -- 4.2 Adding of New Entries -- 4.3 Removing of Existing Entries -- 4.4 Running Times -- 5 Conclusions -- References -- Clustering and Identification of Core Implications -- 1 Introduction. 2 Previous Works on FCA and Clustering -- 3 Background and the fcaR package -- 4 Proposed Research Line -- 5 Experimental Results -- 6 Conclusions -- References -- Extracting Relations in Texts with Concepts of Neighbours -- 1 Introduction -- 2 Preliminaries -- 3 Modeling Sentences as Graphs -- 3.1 NLP Treatments -- 3.2 Sentences as an RDF Graph -- 3.3 Type Hierarchies -- 4 Relation Extraction with Concepts of Neighbours -- 4.1 Concepts of Neighbours for Relation Extraction in Texts -- 4.2 Scoring Methods -- 5 Experiments -- 5.1 Dataset and Baseline -- 5.2 Experimental Settings -- 5.3 Quantitative Results -- 5.4 Qualitative Results -- 6 Conclusion -- References -- Exploration and Visualisation -- Triadic Exploration and Exploration with Multiple Experts -- 1 Introduction -- 2 Dyadic and Triadic Formal Contexts -- 2.1 Formal Concept Analysis -- 2.2 Triadic Concept Analysis -- 2.3 Attribute Implications -- 2.4 Attribute Exploration -- 3 Triadic Exploration -- 3.1 Conditional Attribute Implications -- 3.2 Triadic Exploration -- 3.3 An Example for Triadic Exploration -- 4 Application for Exploration with Multiple Experts -- 5 Conclusion and Outlook -- References -- Towards Interactive Transition from AOC Poset to Concept Lattice -- 1 Introduction -- 1.1 Formal Concept Analysis and Scalability -- 1.2 AOC Poset -- 1.3 Morphing AOC Poset into Concept Lattice -- 1.4 Generating only Abstract Concepts -- 1.5 Organisation -- 2 Context Ablation -- 2.1 Preliminaries -- 2.2 Strategy -- 2.3 Elimination of Bigraph Elements -- 2.4 Iterative Edge Elimination -- 3 Formal Concept Analysis of Ablated Context -- 3.1 Finding Valid Abstract Concepts -- 3.2 Dividing and Conquering -- 3.3 Anticipating and Localising Change in the AOC Poset -- 4 Discussion and Summary -- References -- Visualization of Statistical Information in Concept Lattice Diagrams. Force-Directed Layout of Order Diagrams Using Dimensional Reduction -- 1 Introduction -- 2 Related Work -- 3 Fundamentals and Basics -- 3.1 Mathematical Notations and Definitions -- 3.2 Force-Directed Graph Drawing -- 4 The ReDraw Algorithm -- 4.1 Node Step -- 4.2 Line Step -- 4.3 Dimension Reduction -- 5 Evaluation -- 5.1 Run-Time Complexity -- 5.2 Tested Datasets -- 5.3 Recommended Parametrizations -- 5.4 Empirical Evaluation -- 5.5 User Evaluation -- 6 Conclusion and Outlook -- References -- Short Papers -- Sandwich: An Algorithm for Discovering Relevant Link Keys in an LKPS Concept Lattice -- 1 Introduction -- 2 The Discovery of Link Keys with Pattern Structures -- 2.1 A Definition of Link Keys -- 2.2 A Pattern Structure for Link Key Discovery -- 3 The Pruning of an lkps-lattice -- 3.1 Correction and Completeness of a Link Key Candidate -- 3.2 Sandwich: An Algorithm for Selecting the Most Relevant Link Key Candidates -- 4 Discussion and Conclusion -- References -- Decision Concept Lattice vs. Decision Trees and Random Forests -- 1 Introduction -- 2 Basic Definitions -- 3 Construct a Concept Lattice via a Set of Decision Trees -- 4 Decision Lattice -- 5 Experiments -- 6 Conclusions -- References -- Exploring Scale-Measures of Data Sets -- 1 Introduction -- 2 Scales and Measurement -- 3 Ideals in the Lattice of Closure Systems -- 4 Recommending Conceptual Scale-Measures -- 5 Related Work -- 6 Conclusion -- References -- Filters, Ideals and Congruences on Double Boolean Algebras -- 1 Introduction -- 2 Concepts, Protoconcepts and Double Boolean Algebras -- 3 Filters and Ideals of a Double Boolean Algebra -- 4 Congruence on Double Boolean Algebras -- 5 Conclusion -- References -- Diagrammatic Representation of Conceptual Structures -- 1 Introduction -- 2 FCA and SCA Notions -- 3 Tabular, Euler and Hasse Diagrams. 4 Obtaining an Observationally Efficient Diagram -- 5 Conclusion -- References -- Author Index.
Record Nr.	UNISA-996464493303316

Pubbl/distr/stampa	London : , : ISTE
Descrizione fisica	1 online resource (376 pages)
Disciplina	385.0285/53
Altri autori (Persone)	BoulangerJean-Louis
Collana	Industrial implementation of formal methods series
Soggetto topico	Railroads - Management - Data processing Formal methods (Computer science) Application software - Development
ISBN	1-118-61437-2 1-118-56189-9 1-299-31507-0 1-118-61438-0
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	From classic languages to formal methods -- Formal method in railway, the first complex application : SAET-METEOR -- B method and B tools -- Model-based design using Simulink : modeling, code generation, verification, and validation -- Proof of global properties with the aid of the Simulink Design verifier proof tool -- SCADE : implementation and applications -- GATel : a V & V platform for scade models -- Control build.
Record Nr.	UNINA-9910139052403321