Applied formal methods--FM-Trends 98 : International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, October 7-9, 1998 : proceedings / / Dieter Hutter (eds.) |
Edizione | [1st ed. 1999.] |
Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [1999] |
Descrizione fisica | 1 online resource (390 p.) |
Disciplina | 005.13/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Formal methods (Computer science) |
ISBN |
1-280-95677-1
9786610956777 3-540-48257-1 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- High Level System Design and Analysis Using Abstract State Machines -- Enriching the Software Development Process by Formal Methods -- Regular Papers -- Formal Program Development in Geometric Modeling -- Design of Distributed Multimedia Applications (DAMD) -- Structured Formal Verification of a Fragment of the IBM S/390 Clock Chip -- Automated Test Set Generation for Statecharts -- Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct -- Translation Validation: From DC+ to C -- A Practical Hierarchical Design by Timed Simulation Relations for Real-Time Systems -- A Lightweight Approach to Formal Methods -- An Open Environment for the Integration of Heterogeneous Modelling Techniques and Tools -- Integrating Domain Specific Language Design in the Software Life Cycle -- Flexible and Reliable Process Model Properties: An Integrated Approach -- A Symbolic Model Checker for ACTL -- Critical Systems Validation and Verification with CSP and FDR -- UniForM Perspectives for Formal Methods -- The UniForM WorkBench A Higher Order Tool Integration Framework -- Application Papers -- Two Real Formal Verification Experiences: ATM Switch Chip and Parallel Cache Protocol -- Formal Methods in the Specification of the Emergency Closing System of the Eastern Scheldt Storm Surge Barrier -- The New Topicality of Using Formal Models of Security Policy within the Security Engineering Process -- Tool Papers -- Towards Comprehensive Tool Support for Abstract State Machines: The ASM Workbench Tool Environment and Architecture -- The IFAD VDM Tools -- KIV 3.0 for Provably Correct Systems -- PVS: An Experience Report -- Overview over the Project Quest -- VSE: Controlling the Complexity in Formal Software Developments -- The wHOLe System -- Z/EVES Version 1.5: An Overview. |
Record Nr. | UNISA-996465943703316 |
Berlin, Germany ; ; New York, New York : , : Springer, , [1999] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Communicating embedded systems [[electronic resource] ] : software and design : formal methods / / edited by Claude Jard, Olivier H. Roux |
Edizione | [1st edition] |
Pubbl/distr/stampa | London, : ISTE |
Descrizione fisica | 1 online resource (275 p.) |
Disciplina | 621.39/2 |
Altri autori (Persone) |
JardClaude
RouxOlivier H |
Collana | ISTE |
Soggetto topico |
Embedded computer systems - Programming
Embedded computer systems - Design and construction Computer software - Development Formal methods (Computer science) |
ISBN |
1-118-55818-9
1-118-60009-6 1-118-60012-6 1-299-18745-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Cover; Communicating Embedded Systems; Title Page; Copyright Page; Table of Contents; Preface; Chapter 1. Models for Real-Time Embedded Systems; 1.1. Introduction; 1.1.1. Model-checking and control problems; 1.1.2. Timed models; 1.2. Notations, languages and timed transition systems; 1.3. Timed models; 1.3.1. Timed Automata; 1.3.2. Time Petri nets; 1.3.2.1. T-time Petri nets; 1.3.2.2. Timed-arc petri nets; 1.3.3. Compared expressiveness of several classes of timed models; 1.3.3.1. Bisimulation and expressiveness of timed models; 1.3.3.2. Compared expressiveness of different classes of TPN
1.3.3.3. Compared expressiveness of TA, TPN, and TAPN1.4. Models with stopwatches; 1.4.1. Formal models for scheduling aspects; 1.4.1.1. Automata and scheduling; 1.4.1.2. Time Petri nets and scheduling; 1.4.2. Stopwatch automata; 1.4.3. Scheduling time Petri nets; 1.4.4. Decidability results for stopwatch models; 1.5. Conclusion; 1.6. Bibliography; Chapter 2. Timed Model-Checking; 2.1. Introduction; 2.2. Timed models; 2.2.1. Timed transition system; 2.2.2. Timed automata; 2.2.3. Other models; 2.3. Timed logics; 2.3.1. Temporal logics CTL and LTL; 2.3.2. Timed extensions; 2.3.2.1. Timed CTL 2.3.2.2. Timed LTL2.4. Timed model-checking; 2.4.1. Model-checking LTL and CTL (untimed case); 2.4.2. Region automaton; 2.4.3. Model-checking TCTL; 2.4.4. Model-checking MTL; 2.4.5. Efficient model-checking; 2.4.6. Model-checking in practice; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Control of Timed Systems; 3.1. Introduction; 3.1.1. Verification of timed systems; 3.1.2. The controller synthesis problem; 3.1.3. From control to game; 3.1.4. Game objectives; 3.1.5. Varieties of untimed games; 3.2. Timed games; 3.2.1. Timed game automata; 3.2.2. Strategies and course of the game 3.2.2.1. The course of a timed game3.2.2.2. Strategies; 3.3. Computation of winning states and strategies; 3.3.1. Controllable predecessors; 3.3.2. Symbolic operators; 3.3.3. Symbolic computation of winning states; 3.3.4. Synthesis of winning strategies; 3.4. Zeno strategies; 3.5. Implementability; 3.5.1. Hybrid automata; 3.5.2. On the existence of non-implementable continuous controllers; 3.5.3. Recent results and open problems; 3.6. Specification of control objectives; 3.7. Optimal control; 3.7.1. TA with costs; 3.7.2. Optimal cost in timed games; 3.7.3. Computation of the optimal cost 3.7.4. Recent results and open problems3.8. Efficient algorithms for controller synthesis; 3.8.1. On-the-fly algorithms; 3.8.2. Recent results and open problems; 3.9. Partial observation; 3.10. Changing game rules...; 3.11. Bibliography; Chapter 4. Fault Diagnosis of Timed Systems; 4.1. Introduction; 4.2. Notations; 4.2.1. Timed words and timed languages; 4.2.2. Timed automata; 4.2.3. Region graph of a TA; 4.2.4. Product of TA; 4.2.5. Timed automata with faults; 4.3. Fault diagnosis problems; 4.3.1. Diagnoser; 4.3.2. The problems; 4.3.3. Necessary and sufficient condition for diagnosability 4.4. Fault diagnosis for discrete event systems |
Record Nr. | UNINA-9910138854403321 |
London, : ISTE | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Communicating embedded systems [[electronic resource] ] : software and design : formal methods / / edited by Claude Jard, Olivier H. Roux |
Edizione | [1st edition] |
Pubbl/distr/stampa | London, : ISTE |
Descrizione fisica | 1 online resource (275 p.) |
Disciplina | 621.39/2 |
Altri autori (Persone) |
JardClaude
RouxOlivier H |
Collana | ISTE |
Soggetto topico |
Embedded computer systems - Programming
Embedded computer systems - Design and construction Computer software - Development Formal methods (Computer science) |
ISBN |
1-118-55818-9
1-118-60009-6 1-118-60012-6 1-299-18745-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Cover; Communicating Embedded Systems; Title Page; Copyright Page; Table of Contents; Preface; Chapter 1. Models for Real-Time Embedded Systems; 1.1. Introduction; 1.1.1. Model-checking and control problems; 1.1.2. Timed models; 1.2. Notations, languages and timed transition systems; 1.3. Timed models; 1.3.1. Timed Automata; 1.3.2. Time Petri nets; 1.3.2.1. T-time Petri nets; 1.3.2.2. Timed-arc petri nets; 1.3.3. Compared expressiveness of several classes of timed models; 1.3.3.1. Bisimulation and expressiveness of timed models; 1.3.3.2. Compared expressiveness of different classes of TPN
1.3.3.3. Compared expressiveness of TA, TPN, and TAPN1.4. Models with stopwatches; 1.4.1. Formal models for scheduling aspects; 1.4.1.1. Automata and scheduling; 1.4.1.2. Time Petri nets and scheduling; 1.4.2. Stopwatch automata; 1.4.3. Scheduling time Petri nets; 1.4.4. Decidability results for stopwatch models; 1.5. Conclusion; 1.6. Bibliography; Chapter 2. Timed Model-Checking; 2.1. Introduction; 2.2. Timed models; 2.2.1. Timed transition system; 2.2.2. Timed automata; 2.2.3. Other models; 2.3. Timed logics; 2.3.1. Temporal logics CTL and LTL; 2.3.2. Timed extensions; 2.3.2.1. Timed CTL 2.3.2.2. Timed LTL2.4. Timed model-checking; 2.4.1. Model-checking LTL and CTL (untimed case); 2.4.2. Region automaton; 2.4.3. Model-checking TCTL; 2.4.4. Model-checking MTL; 2.4.5. Efficient model-checking; 2.4.6. Model-checking in practice; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Control of Timed Systems; 3.1. Introduction; 3.1.1. Verification of timed systems; 3.1.2. The controller synthesis problem; 3.1.3. From control to game; 3.1.4. Game objectives; 3.1.5. Varieties of untimed games; 3.2. Timed games; 3.2.1. Timed game automata; 3.2.2. Strategies and course of the game 3.2.2.1. The course of a timed game3.2.2.2. Strategies; 3.3. Computation of winning states and strategies; 3.3.1. Controllable predecessors; 3.3.2. Symbolic operators; 3.3.3. Symbolic computation of winning states; 3.3.4. Synthesis of winning strategies; 3.4. Zeno strategies; 3.5. Implementability; 3.5.1. Hybrid automata; 3.5.2. On the existence of non-implementable continuous controllers; 3.5.3. Recent results and open problems; 3.6. Specification of control objectives; 3.7. Optimal control; 3.7.1. TA with costs; 3.7.2. Optimal cost in timed games; 3.7.3. Computation of the optimal cost 3.7.4. Recent results and open problems3.8. Efficient algorithms for controller synthesis; 3.8.1. On-the-fly algorithms; 3.8.2. Recent results and open problems; 3.9. Partial observation; 3.10. Changing game rules...; 3.11. Bibliography; Chapter 4. Fault Diagnosis of Timed Systems; 4.1. Introduction; 4.2. Notations; 4.2.1. Timed words and timed languages; 4.2.2. Timed automata; 4.2.3. Region graph of a TA; 4.2.4. Product of TA; 4.2.5. Timed automata with faults; 4.3. Fault diagnosis problems; 4.3.1. Diagnoser; 4.3.2. The problems; 4.3.3. Necessary and sufficient condition for diagnosability 4.4. Fault diagnosis for discrete event systems |
Record Nr. | UNINA-9910820091003321 |
London, : ISTE | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Complex data analytics with formal concept analysis / / Rokia Missaoui, Léonard Kwuida, and Talel Abdessalem |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2022] |
Descrizione fisica | 1 online resource (277 pages) |
Disciplina | 004.0151 |
Soggetto topico |
Formal methods (Computer science)
Data mining |
ISBN | 3-030-93278-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996478862203316 |
Cham, Switzerland : , : Springer International Publishing, , [2022] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Complex data analytics with formal concept analysis / / Rokia Missaoui, Léonard Kwuida, and Talel Abdessalem |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2022] |
Descrizione fisica | 1 online resource (277 pages) |
Disciplina | 004.0151 |
Soggetto topico |
Formal methods (Computer science)
Data mining |
ISBN | 3-030-93278-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNINA-9910735392703321 |
Cham, Switzerland : , : Springer International Publishing, , [2022] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Composing model-based analysis tools / / edited by Robert Heinrich [and three others] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
Descrizione fisica | 1 online resource (311 pages) |
Disciplina | 004.0151 |
Soggetto topico |
Formal methods (Computer science)
Software engineering |
ISBN | 3-030-81915-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNINA-9910512176003321 |
Cham, Switzerland : , : Springer, , [2021] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Composing model-based analysis tools / / edited by Robert Heinrich [and three others] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
Descrizione fisica | 1 online resource (311 pages) |
Disciplina | 004.0151 |
Soggetto topico |
Formal methods (Computer science)
Software engineering |
ISBN | 3-030-81915-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996464445703316 |
Cham, Switzerland : , : Springer, , [2021] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Computer performance engineering : 5th European Performance Engineering Workshop, EPEW 2008, Palma de Mallorca, Spain, September 24-25, 2008 : proceedings / / Nigel Thomas, Carlos Juiz (editors) |
Edizione | [1st ed. 2008.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2008] |
Descrizione fisica | 1 online resource (X, 272 p.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-540-87412-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Performance and Dependability Evaluation: Successes, Failures and Challenges -- Partial Evaluation of PEPA Models for Fluid-Flow Analysis -- Software Performance Engineering -- An Empirical Investigation of the Applicability of a Component-Based Performance Prediction Method -- A Calibration Framework for Capturing and Calibrating Software Performance Models -- Performance Evaluation of Embedded ECA Rule Engines: A Case Study -- Stochastic Process Algebra and SANs -- Towards State Space Reduction Based on T-Lumpability-Consistent Relations -- A Ticking Clock: Performance Analysis of a Circadian Rhythm with Stochastic Process Algebra -- Assembly Code Analysis Using Stochastic Process Algebra -- Product Form Steady-State Distribution for Stochastic Automata Networks with Domino Synchronizations -- Performance Query Specification and Measurement -- State-Aware Performance Analysis with eXtended Stochastic Probes -- Computer and Communications Networks -- Natural Language Specification of Performance Trees -- Recurrent Method for Blocking Probability Calculation in Multi-service Switching Networks with BPP Traffic -- An Approximate Model of the WCDMA Interface Servicing a Mixture of Multi-rate Traffic Streams with Priorities -- Queueing Theory and Markov Chains -- Performance Analysis of Dynamic Priority Shifting -- Performance Analysis of a Priority Queue with Place Reservation and General Transmission Times -- Analysis of BMAP/G/1 Vacation Model of Non-M/G/1-Type -- Applications -- Stochastic Bounds for Partially Generated Markov Chains: An Algebraic Approach -- Evaluation of P2P Algorithms for Probabilistic Trust Inference in a Web of Trust -- Approximation for Multi-service Systems with Reservation by Systems with Limited-Availability. |
Record Nr. | UNINA-9910484395703321 |
Berlin ; ; Heidelberg : , : Springer, , [2008] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Computer performance engineering : 5th European Performance Engineering Workshop, EPEW 2008, Palma de Mallorca, Spain, September 24-25, 2008 : proceedings / / Nigel Thomas, Carlos Juiz (editors) |
Edizione | [1st ed. 2008.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2008] |
Descrizione fisica | 1 online resource (X, 272 p.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico | Formal methods (Computer science) |
ISBN | 3-540-87412-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Performance and Dependability Evaluation: Successes, Failures and Challenges -- Partial Evaluation of PEPA Models for Fluid-Flow Analysis -- Software Performance Engineering -- An Empirical Investigation of the Applicability of a Component-Based Performance Prediction Method -- A Calibration Framework for Capturing and Calibrating Software Performance Models -- Performance Evaluation of Embedded ECA Rule Engines: A Case Study -- Stochastic Process Algebra and SANs -- Towards State Space Reduction Based on T-Lumpability-Consistent Relations -- A Ticking Clock: Performance Analysis of a Circadian Rhythm with Stochastic Process Algebra -- Assembly Code Analysis Using Stochastic Process Algebra -- Product Form Steady-State Distribution for Stochastic Automata Networks with Domino Synchronizations -- Performance Query Specification and Measurement -- State-Aware Performance Analysis with eXtended Stochastic Probes -- Computer and Communications Networks -- Natural Language Specification of Performance Trees -- Recurrent Method for Blocking Probability Calculation in Multi-service Switching Networks with BPP Traffic -- An Approximate Model of the WCDMA Interface Servicing a Mixture of Multi-rate Traffic Streams with Priorities -- Queueing Theory and Markov Chains -- Performance Analysis of Dynamic Priority Shifting -- Performance Analysis of a Priority Queue with Place Reservation and General Transmission Times -- Analysis of BMAP/G/1 Vacation Model of Non-M/G/1-Type -- Applications -- Stochastic Bounds for Partially Generated Markov Chains: An Algebraic Approach -- Evaluation of P2P Algorithms for Probabilistic Trust Inference in a Web of Trust -- Approximation for Multi-service Systems with Reservation by Systems with Limited-Availability. |
Record Nr. | UNISA-996466091603316 |
Berlin ; ; Heidelberg : , : Springer, , [2008] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Computers in language research [[electronic resource] ] . 2 / / edited by Walter A. Sedelow, Jr., Sally Yeates Sedelow |
Edizione | [Reprint 2011] |
Pubbl/distr/stampa | Berlin ; ; New York, : Mouton Publishers, c1983 |
Descrizione fisica | 1 online resource (312 p.) |
Disciplina | 410/.28/5 |
Altri autori (Persone) |
SedelowWalter A
SedelowSally Yeates <1931-> |
Collana |
Trends in Linguistics. Studies and Monographs [TiLSM]
Trends in linguistics. |
Soggetto topico |
Computational linguistics
Music - Data processing Formal languages Formal methods (Computer science) |
Soggetto genere / forma | Electronic books. |
ISBN | 3-11-082334-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | pt. 1. Formalization in literary and discourse analysis -- pt. 2. Notating the language of music and the (pause) rhythms of speech. |
Record Nr. | UNINA-9910461913803321 |
Berlin ; ; New York, : Mouton Publishers, c1983 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|