Formal Techniques in Real-Time and Fault-Tolerant Systems [[electronic resource] ] : Second International Symposium, Nijmegen, The Netherlands, January 8-10, 1992. Proceedings / / edited by Jan Vytopil |
Edizione | [1st ed. 1991.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1991 |
Descrizione fisica | 1 online resource (XII, 628 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Applied mathematics Engineering mathematics Mathematical logic Computer logic Probabilities Statistics Theory of Computation Applications of Mathematics Mathematical Logic and Foundations Logics and Meanings of Programs Probability Theory and Stochastic Processes Statistics, general |
ISBN | 3-540-46692-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | ISL: An interval logic for the specification of real-time programs -- Duration specifications for shared processors -- A compositional semantics for fault-tolerant real-time systems -- Modelling real-time behavior with an interval time calculus -- Multicycles and RTL logic satisfiability -- Voluntary preemption: A tool in the design of hard real-time systems -- Observing task preemption in Ada 9X -- Real-time scheduling by queue automata -- Broadcast communication for real-time processes -- Analysis of timeliness requirements in safety-critical systems -- Verification of a reliable net protocol -- Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization -- Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems -- On fault-tolerant symbolic computations -- Temporal logic applied to reliability modelling of fault-tolerant systems -- Specifying asynchronous transfer of control -- Protocol design by layered decomposition -- Scheduling in Real-Time Models -- A temporal approach to requirements specification of real-time systems -- RLucid, a general real-time dataflow language -- A mechanized theory for the verification of real-time program code using higher order logic -- Specification and verification of real-time behaviour using Z and RTL -- TAM: A formal framework for the development of distributed real-time systems -- An attempt to confront asynchronous reality to synchronous modelization in the ESTEREL language -- The real-time behaviour of asynchronously communicating processes -- Asynchronous communication in real space process algebra -- Translating timed process algebra into prioritized process algebra -- Operational semantics for timed observations -- Real-timed concurrent refineable behaviours -- Stepwise development of model-oriented real-time specifications from action/event models -- Formal specification of fault tolerant real time systems using minimal 3-sorted modal logic -- Timed and Hybrid Statecharts and their textual representation. |
Record Nr. | UNISA-996465330903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1991 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Fourth IEEE Real-Time Technology and Applications Symposium : proceedings, Denver, Colorado, June 3-5, 1998 |
Pubbl/distr/stampa | [Place of publication not identified], : IEEE Computer Society Press, 1998 |
Disciplina | 004/.33 |
Soggetto topico |
Real-time data processing - Congresses
Real-time control - Congresses Engineering & Applied Sciences Computer Science |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996217750003316 |
[Place of publication not identified], : IEEE Computer Society Press, 1998 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Fourth International Workshop on Real-Time Computing Systems and Applications : proceedings, October 27-29, 1997, Academia Sinica, Taipei, Taiwan, ROC |
Pubbl/distr/stampa | [Place of publication not identified], : IEEE Computer Society Press, 1997 |
Disciplina | 004/.33 |
Soggetto topico |
Real-time data processing
Engineering & Applied Sciences Computer Science |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996204519303316 |
[Place of publication not identified], : IEEE Computer Society Press, 1997 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
FSM-based digital design using Verilog HDL [[electronic resource] /] / Peter Minns, Ian Elliott |
Autore | Minns Peter D |
Edizione | [1st edition] |
Pubbl/distr/stampa | Chichester, England ; ; Hoboken, NJ, : J. Wiley & Sons, c2008 |
Descrizione fisica | 1 online resource (409 p.) |
Disciplina | 004/.33 |
Altri autori (Persone) | ElliottIan D |
Soggetto topico |
Verilog (Computer hardware description language)
Digital electronics Sequential machine theory |
ISBN |
1-282-34988-0
9786612349881 0-470-98762-6 0-470-98761-8 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
FSM-based Digital Design using Verilog HDL; Contents; Preface; Acknowledgements; 1 Introduction to Finite-State Machines and State Diagrams for the Design of Electronic Circuits and Systems; 1.1 INTRODUCTION; 1.2 LEARNING MATERIAL; 1.3 SUMMARY; 2 Using State Diagrams to Control External Hardware Subsystems; 2.1 INTRODUCTION; 2.2 LEARNING MATERIAL; 2.3 SUMMARY; 3 Synthesizing Hardware from a State Diagram; 3.1 INTRODUCTION TO FINITE-STATE MACHINE SYNTHESIS; 3.2 LEARNING MATERIAL; 3.3 SUMMARY; 4 Synchronous Finite-State Machine Designs; 4.1 TRADITIONAL STATE DIAGRAM SYNTHESIS METHOD
4.2 DEALING WITH UNUSED STATES4.3 DEVELOPMENT OF A HIGH/LOW ALARM INDICATOR SYSTEM; 4.3.1 Testing the Finite-State Machine using a Test-Bench Module; 4.4 SIMPLE WAVEFORM GENERATOR; 4.4.1 Sampling Frequency and Samples per Waveform; 4.5 THE DICE GAME; 4.5.1 Development of the Equations for the Dice Game; 4.6 BINARY DATA SERIAL TRANSMITTER; 4.6.1 The RE Counter Block in the Shift Register of Figure 4.15; 4.7 DEVELOPMENT OF A SERIAL ASYNCHRONOUS RECEIVER; 4.7.1 Finite-State Machine Equations; 4.8 ADDING PARITY DETECTION TO THE SERIAL RECEIVER SYSTEM; 4.8.1 To Incorporate the Parity 4.8.2 D-Type Equations for Figure 4.264.9 AN ASYNCHRONOUS SERIAL TRANSMITTER SYSTEM; 4.9.1 Equations for the Asynchronous Serial Transmitter; 4.10 CLOCKED WATCHDOG TIMER; 4.10.1 D Flip-Flop Equations; 4.10.2 Output Equation; 4.11 SUMMARY; 5 The One Hot Technique in Finite-State Machine Design; 5.1 THE ONE HOT TECHNIQUE; 5.2 A DATA ACQUISITION SYSTEM; 5.3 A SHARED MEMORY SYSTEM; 5.4 FAST WAVEFORM SYNTHESIZER; 5.4.1 Specification; 5.4.2 A Possible Solution; 5.4.3 Equations for the d Inputs to D Flip-Flops; 5.4.4 Output Equations 5.5 CONTROLLING THE FINITE-STATE MACHINE FROM A MICROPROCESSOR/MICROCONTROLLER5.6 A MEMORY-CHIP TESTER; 5.7 COMPARING ONE HOT WITH THE MORE CONVENTIONAL DESIGN METHOD OF CHAPTER 4; 5.8 A DYNAMIC MEMORY ACCESS CONTROLLER; 5.8.1 Flip-Flop Equations; 5.8.2 Output Equations; 5.9 HOW TO CONTROL THE DYNAMIC MEMORY ACCESS FROM A MICROPROCESSOR; 5.10 DETECTING SEQUENTIAL BINARY SEQUENCES USING A FINITE-STATE MACHINE; 5.11 SUMMARY; 6 Introduction to Verilog HDL; 6.1 A BRIEF BACKGROUND TO HARDWARE DESCRIPTION LANGUAGES; 6.2 HARDWARE MODELLING WITH VERILOG HDL: THE MODULE 6.3 MODULES WITHIN MODULES: CREATING HIERARCHY6.4 VERILOG HDL SIMULATION: A COMPLETE EXAMPLE; REFERENCES; 7 Elements of Verilog HDL; 7.1 BUILT-IN PRIMITIVES AND TYPES; 7.1.1 Verilog Types; 7.1.2 Verilog Logic and Numeric Values; 7.1.3 Specifying Values; 7.1.4 Verilog HDL Primitive Gates; 7.2 OPERATORS AND EXPRESSIONS; 7.3 EXAMPLE ILLUSTRATING THE USE OF VERILOG HDL OPERATORS: HAMMING CODE ENCODER; 7.3.1 Simulating the Hamming Encoder; REFERENCES; 8 Describing Combinational and Sequential Logic using Verilog HDL; 8.1 THE DATA-FLOW STYLE OF DESCRIPTION: REVIEW OF THE CONTINUOUS ASSIGNMENT 8.2 THE BEHAVIOURAL STYLE OF DESCRIPTION: THE SEQUENTIAL BLOCK |
Record Nr. | UNINA-9910144431803321 |
Minns Peter D
![]() |
||
Chichester, England ; ; Hoboken, NJ, : J. Wiley & Sons, c2008 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
FSM-based digital design using Verilog HDL [[electronic resource] /] / Peter Minns, Ian Elliott |
Autore | Minns Peter D |
Edizione | [1st edition] |
Pubbl/distr/stampa | Chichester, England ; ; Hoboken, NJ, : J. Wiley & Sons, c2008 |
Descrizione fisica | 1 online resource (409 p.) |
Disciplina | 004/.33 |
Altri autori (Persone) | ElliottIan D |
Soggetto topico |
Verilog (Computer hardware description language)
Digital electronics Sequential machine theory |
ISBN |
1-282-34988-0
9786612349881 0-470-98762-6 0-470-98761-8 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
FSM-based Digital Design using Verilog HDL; Contents; Preface; Acknowledgements; 1 Introduction to Finite-State Machines and State Diagrams for the Design of Electronic Circuits and Systems; 1.1 INTRODUCTION; 1.2 LEARNING MATERIAL; 1.3 SUMMARY; 2 Using State Diagrams to Control External Hardware Subsystems; 2.1 INTRODUCTION; 2.2 LEARNING MATERIAL; 2.3 SUMMARY; 3 Synthesizing Hardware from a State Diagram; 3.1 INTRODUCTION TO FINITE-STATE MACHINE SYNTHESIS; 3.2 LEARNING MATERIAL; 3.3 SUMMARY; 4 Synchronous Finite-State Machine Designs; 4.1 TRADITIONAL STATE DIAGRAM SYNTHESIS METHOD
4.2 DEALING WITH UNUSED STATES4.3 DEVELOPMENT OF A HIGH/LOW ALARM INDICATOR SYSTEM; 4.3.1 Testing the Finite-State Machine using a Test-Bench Module; 4.4 SIMPLE WAVEFORM GENERATOR; 4.4.1 Sampling Frequency and Samples per Waveform; 4.5 THE DICE GAME; 4.5.1 Development of the Equations for the Dice Game; 4.6 BINARY DATA SERIAL TRANSMITTER; 4.6.1 The RE Counter Block in the Shift Register of Figure 4.15; 4.7 DEVELOPMENT OF A SERIAL ASYNCHRONOUS RECEIVER; 4.7.1 Finite-State Machine Equations; 4.8 ADDING PARITY DETECTION TO THE SERIAL RECEIVER SYSTEM; 4.8.1 To Incorporate the Parity 4.8.2 D-Type Equations for Figure 4.264.9 AN ASYNCHRONOUS SERIAL TRANSMITTER SYSTEM; 4.9.1 Equations for the Asynchronous Serial Transmitter; 4.10 CLOCKED WATCHDOG TIMER; 4.10.1 D Flip-Flop Equations; 4.10.2 Output Equation; 4.11 SUMMARY; 5 The One Hot Technique in Finite-State Machine Design; 5.1 THE ONE HOT TECHNIQUE; 5.2 A DATA ACQUISITION SYSTEM; 5.3 A SHARED MEMORY SYSTEM; 5.4 FAST WAVEFORM SYNTHESIZER; 5.4.1 Specification; 5.4.2 A Possible Solution; 5.4.3 Equations for the d Inputs to D Flip-Flops; 5.4.4 Output Equations 5.5 CONTROLLING THE FINITE-STATE MACHINE FROM A MICROPROCESSOR/MICROCONTROLLER5.6 A MEMORY-CHIP TESTER; 5.7 COMPARING ONE HOT WITH THE MORE CONVENTIONAL DESIGN METHOD OF CHAPTER 4; 5.8 A DYNAMIC MEMORY ACCESS CONTROLLER; 5.8.1 Flip-Flop Equations; 5.8.2 Output Equations; 5.9 HOW TO CONTROL THE DYNAMIC MEMORY ACCESS FROM A MICROPROCESSOR; 5.10 DETECTING SEQUENTIAL BINARY SEQUENCES USING A FINITE-STATE MACHINE; 5.11 SUMMARY; 6 Introduction to Verilog HDL; 6.1 A BRIEF BACKGROUND TO HARDWARE DESCRIPTION LANGUAGES; 6.2 HARDWARE MODELLING WITH VERILOG HDL: THE MODULE 6.3 MODULES WITHIN MODULES: CREATING HIERARCHY6.4 VERILOG HDL SIMULATION: A COMPLETE EXAMPLE; REFERENCES; 7 Elements of Verilog HDL; 7.1 BUILT-IN PRIMITIVES AND TYPES; 7.1.1 Verilog Types; 7.1.2 Verilog Logic and Numeric Values; 7.1.3 Specifying Values; 7.1.4 Verilog HDL Primitive Gates; 7.2 OPERATORS AND EXPRESSIONS; 7.3 EXAMPLE ILLUSTRATING THE USE OF VERILOG HDL OPERATORS: HAMMING CODE ENCODER; 7.3.1 Simulating the Hamming Encoder; REFERENCES; 8 Describing Combinational and Sequential Logic using Verilog HDL; 8.1 THE DATA-FLOW STYLE OF DESCRIPTION: REVIEW OF THE CONTINUOUS ASSIGNMENT 8.2 THE BEHAVIOURAL STYLE OF DESCRIPTION: THE SEQUENTIAL BLOCK |
Record Nr. | UNINA-9910818859403321 |
Minns Peter D
![]() |
||
Chichester, England ; ; Hoboken, NJ, : J. Wiley & Sons, c2008 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Interactive Systems: Design, Specification, and Verification [[electronic resource] ] : 8th International Workshop, DSV-IS 2001. Glasgow, Scotland, UK, June 13-15, 2001. Revised Papers / / edited by Chris J. Johnson |
Edizione | [1st ed. 2001.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
Descrizione fisica | 1 online resource (XII, 221 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
User interfaces (Computer systems)
Application software Computer hardware Computer graphics Software engineering Computer logic User Interfaces and Human Computer Interaction Computer Applications Computer Hardware Computer Graphics Software Engineering Logics and Meanings of Programs |
ISBN | 3-540-45522-1 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Mobile Interface Design -- An XML-Based Runtime User Interface Description Language for Mobile Computing Devices -- Model-Based User Interface Design Using Markup Concepts -- Abstract User Interfaces: A Model and Notation to Support Plasticity in Interactive Systems -- Task Modelling for Context-Sensitive User Interfaces -- Supervision and Control Systems -- Industrial User Interface Evaluation Based on Coloured Petri Nets Modelling and Analysis -- A Tool Suite for Integrating Task and System Models through Scenarios -- Temporal and Stochastic Issues -- Temporal Patterns for Complex Interaction Design -- Modelling Dynamic Group Behaviours -- Reasoning about Interactive Systems with Stochastic Models -- New Perspectives -- Towards Uniformed Task Models in a Model-Based Approach -- Heuristic Evaluation of Website Attractiveness and Usability -- Affordance and Symmetry. |
Record Nr. | UNISA-996465934903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Interactive Systems: Design, Specification, and Verification : 8th International Workshop, DSV-IS 2001. Glasgow, Scotland, UK, June 13-15, 2001. Revised Papers / / edited by Chris J. Johnson |
Edizione | [1st ed. 2001.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
Descrizione fisica | 1 online resource (XII, 221 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
User interfaces (Computer systems)
Application software Computer hardware Computer graphics Software engineering Computer logic User Interfaces and Human Computer Interaction Computer Applications Computer Hardware Computer Graphics Software Engineering Logics and Meanings of Programs |
ISBN | 3-540-45522-1 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Mobile Interface Design -- An XML-Based Runtime User Interface Description Language for Mobile Computing Devices -- Model-Based User Interface Design Using Markup Concepts -- Abstract User Interfaces: A Model and Notation to Support Plasticity in Interactive Systems -- Task Modelling for Context-Sensitive User Interfaces -- Supervision and Control Systems -- Industrial User Interface Evaluation Based on Coloured Petri Nets Modelling and Analysis -- A Tool Suite for Integrating Task and System Models through Scenarios -- Temporal and Stochastic Issues -- Temporal Patterns for Complex Interaction Design -- Modelling Dynamic Group Behaviours -- Reasoning about Interactive Systems with Stochastic Models -- New Perspectives -- Towards Uniformed Task Models in a Model-Based Approach -- Heuristic Evaluation of Website Attractiveness and Usability -- Affordance and Symmetry. |
Record Nr. | UNINA-9910768458003321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Operational Semantics for Timed Systems [[electronic resource] ] : A Non-standard Approach to Uniform Modeling of Timed and Hybrid Systems / / by Heinrich Rust |
Autore | Rust Heinrich |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XII, 224 p.) |
Disciplina | 004/.33 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computers Programming languages (Electronic computers) Operating systems (Computers) Mathematical logic Software Engineering Computation by Abstract Devices Programming Languages, Compilers, Interpreters Operating Systems Mathematical Logic and Formal Languages |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996465800903316 |
Rust Heinrich
![]() |
||
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Operational Semantics for Timed Systems : A Non-standard Approach to Uniform Modeling of Timed and Hybrid Systems / / by Heinrich Rust |
Autore | Rust Heinrich |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XII, 224 p.) |
Disciplina | 004/.33 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computers Programming languages (Electronic computers) Operating systems (Computers) Mathematical logic Software Engineering Computation by Abstract Devices Programming Languages, Compilers, Interpreters Operating Systems Mathematical Logic and Formal Languages |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNINA-9910767560703321 |
Rust Heinrich
![]() |
||
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Parallel and Distributed Real-Time Systems, 2nd Workshop |
Pubbl/distr/stampa | [Place of publication not identified], : IEEE Computer Society Press, 1994 |
Disciplina | 004/.33 |
Soggetto topico |
Engineering & Applied Sciences
Computer Science |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996198227203316 |
[Place of publication not identified], : IEEE Computer Society Press, 1994 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|